Constructor Functions

Lars Hupel 🌐

April 19, 2017

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


Isabelle's code generator performs various adaptations for target languages. Among others, constructor applications have to be fully saturated. That means that for constructor calls occuring as arguments to higher-order functions, synthetic lambdas have to be inserted. This entry provides tooling to avoid this construction altogether by introducing constructor functions.
BSD License


Theories of Constructor_Funs

Used by