LeanToolkit

This is a prototype implementation of an inductive type composition framework in Lean. More information can be found at the "Modular Composition of Inductive Types Using Lean Meta-programming" paper.

An installation of Lean 4 (including elan and lake) is required.

To build the project:

lake build

And to run the test cases and the case study:

lake test