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 penalty in order to widen that range.
Larry > On 3 Nov 2016, at 13:46, Makarius <makar...@sketis.net> wrote: > > Luckily the situation is not as bad, and David Matthews continues to > consolidate the new compiler and run-time system: Isabelle is already a > bit faster than before, while still remaining true to mathematical > semantics of int. >
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
