BSD Portswip/rocq 9.2.0 NetBSD
Theorem prover which extracts programs from proofs
- System
- NetBSD
- Repository
- pkgsrc-wip
- Maintainer
- [email protected]
- Port added
- Last update
- Commit
2408ea507e- License
- gnu-lgpl-v2.1
- Categories
- wip, lang, math
Description
Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs consistently with their specifications.
In the other systems
| System | Port | Version |
|---|---|---|
| NetBSD | wip/rocq | 9.2.0 |
| OpenBSD | math/rocq | 8.20.1p2 |
Install
From pkgsrc-wip (no binary package):
cd /usr/pkgsrc/wip/rocq && make install cleanDependencies
Run dependencies 3
No port depends on this one.