Formal proof management system

Edit Package ocaml-coq
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.

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
No comments available
openSUSE Build Service is sponsored by