Agree. And now real (fact k)” must never be used, now that “fact” is also
generic.
This reminds me of a current IDE limitation: there’s currently no way (as far
as I know) to get the type of a nonvariable expression, such as fact k” above.
Larry Paulson
On 2 Jun 2015, at 19:18, Florian
Dear all,
http://isabelle.in.tum.de/reports/Isabelle/rev/838025c6e278 introduces
type classes »(sem)idom_divide« with an explicit partial divide
operations in integral (semi)domains, which specialises smoothly to
field division or euclidean division later on. In _ you see how this
allows to
I believe Maude (another system named after a French female, presumably) even
had a different minus operator on “nat” as opposed to the other types. In a
formal context, such precision is surely helpful. Indeed, minus is a nasty
case for Dmitriy’s coercions.
If there an established infix
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?
b) The conservative solution: partial division has »_ div _«, an (the
more special) field division »_ / _«. This seems more
Dear all,
recently, I stumbled (once again) over the matter of the »real« conversion.
There is an inclusion hierarchy (⊆) of numerical types
(num ⊆) nat ⊆ int ⊆ rat ⊆ real ⊆ complex
We can embed »smaller« into »bigger« types using conversions
(numeral ⊆) of_nat ⊆ of_int ⊆
I also vote for b). I would also like to add that I ran into situations
where I required the notation of an inverse element in a ring. I defined
this as ring_inv x = 1 div x. For instance, on int, we have ring_inv
1 = 1 and ring_inv (-1) = -1 and everything else is basically
ill-defined, because 1
