package rocq-prover

  1. Overview
  2. Docs

Description

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 is a virtual package gathering the rocq-core and rocq-stdlib packages.

Published: 20 Mar 2025

Dependencies (2)

  1. rocq-stdlib
  2. rocq-core

Dev Dependencies

None

Used by (1)

  1. coq-lsp >= "0.2.3+9.0"

Conflicts

None

OCaml

Innovation. Community. Security.