Applications written in Rocq-Elpi

• Derive shows how to obtain proved equality tests and a few extra gadgets out of inductive type declarations. See the README for the list of derivations. It comes bundled with Rocq-Elpi.

• Locker lets one hide the computational contents of definitions via modules or opaque locks. It comes bundled with Rocq-Elpi.

• Hierarchy Builder is a Rocq extension to declare hierarchies of algebraic structures.

• Algebra Tactics is a port of the ring and field tactics to the Mathematical Components library.

• Trakt is a generic goal preprocessing tool for proof automation tactics in Rocq.

• Namespace Emulation System implements most of the features of namespaces (on top of Rocq's modules).

• Dx uses Elpi to generate an intermediate representation of Rocq terms, to be later transformed into C.

• Coercion enables one to program coercions in Elpi. It comes bundled with Rocq-Elpi.

• Record builder implements fancy record build/update syntax. It comes bundled with Rocq-Elpi.