Hi Manuel,
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
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?
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
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
