[isabelle-dev] New handling of int/nat

[René Neumann]

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.

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4782 bytes
Desc: S/MIME Kryptografische Unterschrift
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130912/1c380c94/attachment.bin>