[isabelle-dev] New handling of int/nat
florian.haftmann at informatik.tu-muenchen.de
Wed Sep 11 19:00:42 CEST 2013
> 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,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev