Package rocq-runtime
Core binaries and tools of the Rocq proof management system
Rocq is a formal proof management system. It provides a formal language to
write mathematical definitions, executable algorithms and theorems together
with an environment for semi-interactive development of machine-checked proofs.
This package includes the Rocq prover core binaries, plugins, and tools, but
not the vernacular standard library.
Version: 9.1.1
General Commands | |
| rocq | The Rocq Prover |
| rocqchk | verify compiled Rocq libraries |