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? 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. Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev