Native Word

Andreas Lochbihler 🌐 with contributions from Peter Lammich 🌐

September 17, 2013

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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


Theories of Native_Word