Re: [isabelle-dev] Integers in Poly/ML

2016-11-03 Thread Lawrence Paulson
Just as remark: MetiTarski took a slight performance hit in the transition to the new compiler, happily greatly reversed by my decision to use fixed-precision integers. Of course I would like to use the IDE for Standard ML, but getting started is always more complicated than it looks. Larry

Re: [isabelle-dev] Integers in Poly/ML

2016-11-03 Thread Makarius
On 03/11/16 13:47, Lawrence Paulson wrote: > Just as remark: MetiTarski took a slight performance hit in the > transition to the new compiler, happily greatly reversed by my decision > to use fixed-precision integers. That taken alone would have meant a step backwards: proper integers have become

Re: [isabelle-dev] Integers in Poly/ML

2016-11-03 Thread Lawrence Paulson
Let’s be clear: the semantics of type int is well-defined. It denotes the set of integers over a specific finite range of values, and if this range is exceeded, exception Overflow is raised. If one’s requirements fit within that range of values then there is no rational reason to suffer a

Re: [isabelle-dev] Integers in Poly/ML

2016-11-03 Thread Makarius
On 03/11/16 14:59, Lawrence Paulson wrote: > Let’s be clear: the semantics of type int is well-defined. It denotes > the set of integers over a specific finite range of values, and if this > range is exceeded, exception Overflow is raised. If one’s requirements > fit within that range of values