Maybe we should resurrect the idea of using adhoc overloading for the
real abbreviation.
Florian, does your rework of the generic machinery for syntactic
abbreviations include moving more of the adhoc overloading into HOL?
Then we could setup real as an adhoc overloaded constant and the proof
The situation regarding coercions has become extremely untidy, and I think it
should be cleared up. We have four generic functions:
of_nat :: nat \Rightarrow ‘a::semiring_1
of_int :: int \Rightarrow ‘a::ring_1
of_rat :: rat \Rightarrow ‘a:: field_char_0
of_real ::
Indeed, the warning sign attached to div can be very helpful. Hence b).
Tobias
On 02/06/2015 21:10, Jasmin Blanchette wrote:
Hi Florian,
a) The radical solution: there is only »_ / _« for both field division
and euclidean division. How natural is notation like »a / b * b + a mod
b = a« then?
I think I could live without real: coercions save a lot of the writing.
Moreover, the real_of_foo abbreviations help to avoid type annotations:
I suppose that all of the current occurrences of real could be replaced with
one particular real_of_foo.
For reading (subgoals etc), one could perhaps
For me the main point of real is the ease of writing. If we get rid of some
lemma duplications but trade that in for many type annotations, I am not in favour.
Tobias
On 02/06/2015 20:18, Florian Haftmann wrote:
Dear all,
recently, I stumbled (once again) over the matter of the »real«
Thank you for reminding me of the reading part. My ability to read formulas
decreases quadratically with their length. Trading in real_of_int for real
makes things definitely worse.
I would want to see a concrete figures how much duplication is avoided in the
current theories and how much
