rocqide

The Rocq Prover is an interactive theorem prover, or proof assistant.

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.

Typical applications include the certification of properties of

programming languages (e.g. the CompCert compiler certification project,

or the Bedrock verified low-level programming library), the

formalization of mathematics (e.g. the full formalization of the

Feit-Thompson theorem or homotopy type theory) and teaching.

This package provides RocqIDE, a lightweight IDE for Rocq.