Re: [isabelle] Rounding negative fractions in Isabelle



On 01.10.2015 17:19, Florian Haftmann wrote:
> that is easily made plausible: the units of a ring (in case of int, +1
> and -1) form a field.  In this segment you expect the conventional rules
> of field division to hold:
[...]
> 	-1 div -1 = -1

I guess you meant "-1 div -1 = +1"?





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.