Proof-oriented layout language

Building

It is recommended to create a dedicated opam switch:

opam switch create rocq-9.0.1 5.4.0
eval $(opam env --switch=rocq-9.0.1)

Add the Rocq opam repository:

opam repo add rocq-released https://rocq-prover.github.io/opam/released/
opam update

Install the project dependencies:

opam install . --deps-only

Then you can build the project by running:

dune build

If you need to clean the project:

dune clean

Optional: direnv

With direnv, entering this directory automatically loads the opam rocq-9.0.1 switch.

Code

Naming convention

This repo uses snake_case for most definitions and constructors. Constructor names are prefixed consistently to reflect the type they belong to.