Constructor Functions

Lars Hupel 🌐

April 19, 2017

Abstract

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.

License

BSD License

Topics

Session Constructor_Funs