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.
- Sources inherited from project devel:languages:ocaml
- Download package
-
Checkout Package
osc -A https://api.opensuse.org checkout devel:languages:haxe/ocaml-coq && cd $_
- Create Badge
Refresh
Refresh
Source Files
Filename | Size | Changed |
---|---|---|
_constraints | 0000000594 594 Bytes | |
_service | 0000000695 695 Bytes | |
ocaml-coq-9.0.0.tar.xz | 0004771728 4.55 MB | |
ocaml-coq.changes | 0000000141 141 Bytes | |
ocaml-coq.patch | 0000000332 332 Bytes | |
ocaml-coq.spec | 0000003565 3.48 KB |
Comments 0