Re: [isabelle] Word32/64 ?
This topic is of interest to me. At the isabelle users workshop in
Munich last year I had a long discussion with Florian about precisely
this. The answer seemed to be "not with the current code generator", and
his argument felt convincing enough for me to leave that approach alone.
One approach for high-performance code seems to be going in reverse,
i.e. parsing annotated SML/C/Haskell/whatever into Isabelle, where you
can pick your own translation, but have to pay by having to specify the
That or trying to write your own code generator, which might be...
Peter Lammich wrote:
Is there any code-generator setup to generate 32/(64) bit integers with
modulo-arithmetic, mapped on the corresponding SML type (Word32) ?
In the logic, the type Word.word has the intended behaviour, but how to
get,e.g., "32 word", mapped to SML's "Word32" ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and