[isabelle-dev] Proper sign of gcd / lcm on type int
florian.haftmann at informatik.tu-muenchen.de
Wed Jun 1 22:07:42 CEST 2016
>> Both are ok in my view; ironically, lcm is used more often in
>> Isabelle/ML than gcd. Providing an lcm in the manner of HOL is trivial,
>> Integer.gcd = PolyML.gcd
>> Integer.lcm = abs oo PolyML.lcm
> These two lines are the plan. Is that a good one or a bad one?
I tinkered around with (a) fractions.gcd in Python and (b)
(a) has mixed signs for gcd
(b) has everything normalized
Maybe this is evidence that we are rather free in choosing our sign
rules, and then normalizing could be a legitimate choice, conceeding
that most practical occuring lcm computations concern non-negative
> Presently, I have used PolyML.IntInf.gcd and PolyML.IntInf.lcm for
> rat.ML (see da38571dd5bd). It somehow violates our cozy Isabelle/ML
> library environment to refer to structure PolyML.
> BTW, AFP has special code generator setup for PolyML.IntInf.gcd here:
> Luckily, this is only gcd and not lcm, so it coincides already.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev