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, beca
> 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 infi
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 m
I would be OK with / for integer division, but there would be a lot of
compatibility issues.
Larry
> On 2 Jun 2015, at 19:17, Florian Haftmann
> wrote:
>
> a) The radical solution: there is only »_ / _« for both field division
> and euclidean division. How natural is notation like »a / b * b +
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 H
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 ⊆ of_ra
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 formul
