[isabelle-dev] Printing integers in Isabelle/ML

[Florian Haftmann]

When printing integers, there is a funny historic artefact:

	Library.string_of_int :: int -> string
	  examples 1705, ~42 -- ie. ML syntax

	Library.signed_string_of_int :: int -> string
	  examples 1705, -42 -- ie. conventional syntax

	ML_Syntax.print_int is an alias for Library.string_of_int

What is particularly confusing about string_of_int vs.
signed_string_of_int that actually both return »signed« strings.  The
naive expectation would be something like:

	Library.string_of_int :: int -> string
	  examples 1705, -42 -- ie. conventional syntax

	ML_Syntax.print_int :: int -> string
	  examples 1705, ~42 -- ie. ML syntax

But there would be a considerable amount of code to be checked and
sorted out then -- without support from the type system.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140918/711e3abe/attachment-0001.asc>