BSD Portsmath/rocq 8.20.1p2 OpenBSD
proof assistant based on a typed lambda calculus
- System
- OpenBSD
- Repository
- OpenBSD ports
- Maintainer
- Yozo Toda <[email protected]>
- Categories
- math
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.
Install
Binary package:
pkg_add rocqFrom the ports tree:
cd /usr/ports/math/rocq && make install