On Wed, 10 Feb 2016, David Matthews wrote:
fun f x y = x+y;
that will fall back to the default "int".
Also, all the library functions that use "int" e.g. Array.sub, String.size,
List.length or TextIO.inputN, will still have the fixed precision int.
This reminds me of the situation in SML/NJ, before I spent some efforts to
force int = IntInf.int on it. It includes a somewhat "patched" basis
library like this:
http://isabelle.in.tum.de/repos/isabelle/file/9343649abb09/src/Pure/RAW/proper_int.ML
I'm inclined to think that having a "configure" option would be the
answer.
That would greatly simplify the Isabelle setup, because we always provide
a separately compiled version of Poly/ML.
Since we are about to discontinue SML/NJ altogether, it would allow to
remove the above tricks, and not move them over to Poly/ML.
Makarius
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
