rocq-8.20.1p2
proof assistant based on a typed lambda calculus
Back to search · Project homepage
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
These are ports metadata. Binary availability depends on the release, architecture and mirror. Build and test dependencies are not an installation checklist.
Direct dependencies
Library
Runtime
Build
Used by (1 dependency relationships)
Includes library, runtime, build and test relationships. Results load 100 at a time.