[isabelle-dev] Infix syntax for division?
jasmin.blanchette at inria.fr
Tue Jun 2 21:10:30 CEST 2015
> 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 sensible than the
> other way round since »_ div _« suggests some kind of »incompleteness«.
> Any opinions?
I’d vote for (b). I also find that “div” suggests some incompleteness. It serves as a warning signal; when you try to prove
sum_sq n = n * (n + 1) * (2 * n + 1) div 6
you think twice and rewrite it into
6 * sum_sq n = n * (n + 1) * (2 * n + 1)
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.
More information about the isabelle-dev