Home

The math/rocq port

rocq-8.20.1p0 – proof assistant based on a typed lambda calculus (cvsweb github mirror)

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/

Maintainer

Yozo Toda

Categories

math

Library dependencies

Build dependencies

Run dependencies

Reverse dependencies

Files

Search
OSZAR »