[isabelle-dev] Infix syntax for division?

[Tobias Nipkow]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5112 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150603/83fe81e6/attachment.bin>