[go: up one dir, main page]

package coq

  1. Overview
  2. No Docs
The Coq Proof Assistant

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (41)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

Description

Coq is a formal proof management system. It 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, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching.

Published: 17 Jan 2025

Dependencies (4)

  1. coqide-server = version
  2. coq-stdlib = version
  3. coq-core = version
  4. dune >= "3.6"

Dev Dependencies (1)

  1. odoc with-doc

Used by (6)

  1. binary_tree
  2. coq-catt-plugin
  3. coq-lsp = "0.2.0+8.20" | = "0.2.2+8.20" | = "0.2.3+8.20" | = "0.2.4+8.20" | = "0.2.5+8.20"
  4. coq-serapi >= "8.20.0+0.20.0"
  5. coq-waterproof < "3.1.0+9.0"
  6. why3-coq >= "1.8.0"

Conflicts

None