[isabelle-dev] Integers in Poly/ML

[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 penalty in order to widen that range.

Larry

> On 3 Nov 2016, at 13:46, Makarius <makarius at 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.
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161103/0e57369f/attachment-0002.html>