[isabelle-dev] Proper sign of gcd / lcm on type int
makarius at sketis.net
Fri Jun 3 21:29:54 CEST 2016
On 03/06/16 18:49, David Matthews wrote:
> The Poly/ML implementation was based on the idea that something called a
> "multiple" ought to follow the usual rules of multiplication; nothing
> stronger than that. I don't think I found anything that indicated what
> the sign should be. The GCD code uses GMP's GCD if possible; the LCM
> code is just derived from that.
> I have no strong opinions on this and I'm happy to change it. There's
> also the question of whether to add it to the IntInf structure and
> signature despite the incompatibility with the "official" library
How is the situation wrt. planned updates of the SML Basic Library
Maybe this is a chance to add IntInf.gcd and IntInf.lcm officially,
which a clear specification about the sign, whatever that might be.
More information about the isabelle-dev