The math/rocq port
rocq-8.20.1p0 – proof assistant based on a typed lambda calculus
Description
The Rocq Prover, formerly known as the Coq Proof Assistant, 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.
WWW: https://rocq-prover.org/
- Categories:
-
math
Library dependencies
Build dependencies
Run dependencies