About signs in divisions etc. I found the following paper very useful: http://research.microsoft.com/apps/pubs/default.aspx?id=151917
Maybe someone else will find it useful too. Cheers On Fri, Jun 3, 2016 at 9:29 PM, Makarius <makar...@sketis.net> wrote: > 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 >> definition. > > How is the situation wrt. planned updates of the SML Basic Library > specification? > > Maybe this is a chance to add IntInf.gcd and IntInf.lcm officially, > which a clear specification about the sign, whatever that might be. > > > Makarius > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev