proof assistant based on a typed lambda calculus
Project homepage: https://rocq-prover.org/
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.
Package information
- Ports path
- math/rocq
- Package architecture
- amd64
- Maintainer
- Yozo Toda <yozo@v007.vaio.ne.jp>
- Categories
- math
- Available flavors
- None listed
- Only for architectures
- aarch64, amd64, i386
Ports list build and test dependencies as well as runtime dependencies. pkg_add selects those needed for installation.
Direct dependencies
Library
Runtime
Build
Used by (1 dependency relationships)
Includes library, runtime, build and test dependencies.