Dear Coq users, we are proud to announce the first release of Hierarchy Builder for
Coq 8.10 and 8.11.
Hierarchy Builder (HB) is a high level language to declare hierarchies
of algebraic structures in Coq. The language is compiled down to
modules, records, notations, canonical structures, coercions, etc.
following the discipline of Packed Classes… but the whole point is
that don’t need to know all that if you use HB.
https://github.com/math-comp/hierarchy-builder
HB is implemented in the Elpi λProlog dialect, a high level programming
language well suited to manipulate syntax trees with binders. The Coq-
Elpi plugin lets you run Elpi code inside Coq and provides an extensive
API to access the state of the prover and to define new commands and
tactics.
https://github.com/LPCIC/coq-elpi/
Happy building!
Best regards,
Cyril Cohen, Kazuhiko Sakaguchi and Enrico Tassi