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.

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

Used by

Cite

× 
@article{Constructor_Funs-AFP,
  author  = {Lars Hupel},
  title   = {Constructor Functions},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2017},
  note    = {\url{https://isa-afp.org/entries/Constructor_Funs.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: