[isabelle-dev] Integers in Poly/ML

Makarius makarius at sketis.net
Thu Nov 3 15:54:22 CET 2016


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 then there is no rational reason to
> suffer a penalty in order to widen that range.

Back to field 1.

We need to reboot the project "Enlightment and Rationalism" from some
centuries ago.


	Makarius





More information about the isabelle-dev mailing list