[isabelle-dev] New handling of int/nat

[Florian Haftmann]

Hi René,

> in Isabelle2012 (and 2013?), the types "nat" and "int" where (using
> Efficient_Nat) directly translated into SML's IntInf.int on code_export.
> 
> This does not happen anymore in Isabelle-dev -- here they are now mapped
> to types in Arith.
> 
> The new behavior yields problems when interfacing with the exported code
> to other SML-code (type mismatch). What is the proposed "new" way here?
> Port all definitions to use type "integer" instead of "nat" ("natural"
> also maps to something in Arith)? Or add a 'wrapper' to each definition?:

there are official conversions between all those arithmetic types:
int_of_integer, integer_of_int etc.  These you can generate and rely on
them in your interface code.  So you are free to provide the interfaces
either on the theory level or directly on the target language level.

Hope this helps,
	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: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130911/01e9318a/attachment.sig>