rocq-stdlibversion Documentation on ocaml.org
The Rocq Proof Assistant -- Standard Library
Rocq 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 Rocq Standard Library, that is to say, the set of modules usually bound to the Stdlib.* namespace.
| Author | The Rocq development team, INRIA, CNRS, and contributors |
|---|---|
| License | LGPL-2.1-only |
| Published | |
| Homepage | https://rocq-prover.org |
| Issue Tracker | https://github.com/coq/stdlib/issues |
| Documentation | https://coq.github.io/doc/ |
| Maintainer | The Rocq standard library development team |
| Dependencies | |
| Source [http] | https://github.com/coq/stdlib/releases/download/V9.1.0/stdlib-9.1.0.tar.gz sha512=5a6c01496917b8f23017d9e94af567be68850155a4545bddb067da83eed97237e34d617345942a708b6a4231e00f9bfc8311cd978bf397bb1ef2ea7c25b1a0a3 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/rocq-stdlib/rocq-stdlib.9.1.0/opam |
Required by
- coq-lspwith-test & (=0.2.3+9.0 | >=0.2.4+9.0 & <0.2.5+8.20 | >=0.2.5+9.1)
- coq-waterproof>=3.1.0+9.1
- rocq-prover
- vsrocq-language-server<2.3.4
