Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Constructor Functions

Email Gateway (Aug 22 2022 at 15:25):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,

I’m happy to announce another new tool in the AFP.

Constructor Functions
by Lars Hupel

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.

https://www.isa-afp.org/entries/Constructor_Funs.shtml

Enjoy,
René

Last updated: Apr 25 2024 at 20:15 UTC