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.
> 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