Formal proof management system
https://opam.ocaml.org/packages/coq
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.
- Download package
-
Checkout Package
osc -A https://api.opensuse.org checkout devel:languages:ocaml/ocaml-coq && cd $_
- Create Badge
Refresh
Refresh
Source Files
Filename | Size | Changed |
---|---|---|
_constraints | 0000000594 594 Bytes | |
_service | 0000000701 701 Bytes | |
ocaml-coq-8.19.1.tar.xz | 0005743660 5.48 MB | |
ocaml-coq.changes | 0000000142 142 Bytes | |
ocaml-coq.patch | 0000000388 388 Bytes | |
ocaml-coq.spec | 0000002785 2.72 KB |
Latest Revision
Olaf Hering (olh)
committed
(revision 35)
- Initial version 8.19.1
Comments 0