Native Word

Andreas Lochbihler with contributions from Peter Lammich

17 September 2013


This entry makes machine words and machine arithmetic available for code generation from Isabelle/HOL. It provides a common abstraction that hides the differences between the different target languages. The code generator maps these operations to the APIs of the target languages. Apart from that, we extend the available bit operations on types int and integer, and map them to the operations in the target languages.
BSD License

Change history

[2013-11-06] added conversion function between native words and characters (revision fd23d9a7fe3a)
[2014-03-31] added words of default size in the target language (by Peter Lammich) (revision 25caf5065833)
[2014-10-06] proper test setup with compilation and execution of tests in all target languages (revision 5d7a1c9ae047)
[2017-09-02] added 64-bit words (revision c89f86244e3c)
[2018-07-15] added cast operators for default-size words (revision fc1f1fb8dd30)

Depends On

Used by


Related Entries