[isabelle-dev] New handling of int/nat
rene.neumann at in.tum.de
Thu Sep 12 14:45:26 CEST 2013
Am 11.09.2013 19:00, schrieb 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.
Thanks. I've been a bit reluctant about using the Arith.* functions in
my handwritten SML-code (relying on generated stuff etc), hoping that
there was something automagical. But now where you've stated that it's
the way to go, I've done it like that.
Institut für Informatik (I7)
Technische Universität München
85748 Garching b. München
Office: MI 03.11.055
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 4782 bytes
Desc: S/MIME Kryptografische Unterschrift
More information about the isabelle-dev