Given an inductive type declaration it synthesizes a bunch of useful stuff such as proved equality tests, projections, parametricity relations.
A toy set of tactics implemented in Elpi.
A Namespace Emulation System.
A kit to lock definitions hard.
Given an inductive type declaration it synthesizes a bunch of useful stuff such as proved equality tests, projections, parametricity relations.
A toy set of tactics implemented in Elpi.
A Namespace Emulation System.
A kit to lock definitions hard.