package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b
Description
The Coq proof assistant provides a formal language to write mathematical definitions, executable algorithms, and theorems, together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g., the CompCert compiler certification project and the Bedrock verified low-level programming library), the formalization of mathematics (e.g., the full formalization of the Feit-Thompson theorem and homotopy type theory) and teaching.
Published: 25 Nov 2022
Dependencies (5)
-
zarith
>= "1.11" -
conf-findutils
build -
dune
>= "2.5.1" -
ocamlfind
>= "1.8.1" -
ocaml
>= "4.09.0"
Dev Dependencies
None
Used by (6)
- binary_tree
-
coq-lsp
!= "0.1.6.1+8.17" & < "0.1.7+8.17" | = "0.1.8+8.16" -
coq-serapi
>= "8.16.0+0.16.0" & < "8.17.0+0.17.0" -
coqide
= "8.16.1" - prooftree
-
why3-coq
>= "1.5.1"
Conflicts (2)
On This Page