coq-stdlibversion

The Coq Proof Assistant -- Standard Library

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.

This package includes the Coq Standard Library, that is to say, the set of modules usually bound to the Coq.* namespace.

AuthorThe Coq development team, INRIA, CNRS, and contributors
LicenseLGPL-2.1-only
Published
Homepagehttps://coq.inria.fr/
Issue Trackerhttps://github.com/coq/coq/issues
MaintainerThe Coq development team <coqdev@inria.fr>
Dependencies
Optional dependencies
Source [http] https://github.com/coq/coq/archive/refs/tags/V8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/coq-stdlib/coq-stdlib.8.17.1/opam
Required by