On 02/06/2016 08:19, Manuel Eberl wrote:
I do think that we should enforce the same thing in the ML implementation of gcd/lcm. Any definition of gcd/lcm for integers where either of them may be negative does not make much sense to me. My guess would be that lcm can be negative in the implementation you mentioned because the author defined "lcm a b = a * b / gcd a b" with the unstated assumption that it is only called for non-negative numbers. Or perhaps they thought the sign does not matter.
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 definition.
David _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
