Documentation of Hierarchy Builder

What is Hierarchy Builder?

Hierarchy Builder is a plugin for Rocq that provides high level commands to declare a hierarchy of structures. It turns a synthetic description of a structure into the low-level Rocq commands required to declare the structure, while ensuring that a few good properties hold.

Documentation of Hierarchy Builder

• Hierarchy Builder source code (no functional interactive version yet).