Re: [isabelle] Word32/64 ?

Hi all,

> 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.

to be more precise, what we would need is a tool which inside the logic
lifts operations on type "64 word" to a dedicated type "word64".  What
could already provide helpful assistance is the "transfer" tool by Amine
Chaieb and Jeremy Avigad, whose basic usage can be followed in

Hope this helps



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.