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.
A hook to insert coercions using Elpi.
A handy syntax to build records.
A hook to solve Canonical Structure problems in Elpi.
An alternative Type Class solver written in Elpi.