package rocq-stdlib
The Rocq Proof Assistant -- Standard Library
Install
Dune Dependency
Authors
Maintainers
Sources
stdlib-9.1.0.tar.gz
sha512=5a6c01496917b8f23017d9e94af567be68850155a4545bddb067da83eed97237e34d617345942a708b6a4231e00f9bfc8311cd978bf397bb1ef2ea7c25b1a0a3
Description
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.
Published: 11 Feb 2026
Dependencies (2)
-
rocq-core
>= "9.0" - rocq-runtime
Dev Dependencies
None
Used by (27)
-
coq-flocq
>= "4.2.2" -
coq-kruskal-almostfull
>= "2.0" -
coq-kruskal-finite
>= "2.0" -
coq-kruskal-trees
>= "2.0" - coq-sflib
- coq-stdlib
- rocq-aac-tactics
- rocq-bignums
- rocq-coinduction
- rocq-elpi
- rocq-equations
- rocq-lean-import
- rocq-libhyps
- rocq-metarocq-utils
-
rocq-num-analysis-algebra
>= "2.1.0" -
rocq-num-analysis-fem
>= "2.1.0" -
rocq-num-analysis-lax-milgram
>= "2.1.0" -
rocq-num-analysis-lebesgue
>= "2.1.0" -
rocq-num-analysis-subset
>= "2.1.0" - rocq-ollibs
- rocq-parseque
- rocq-pi-agm
- rocq-relation-algebra
- rocq-semantics
- rocq-typed-extraction-common
- rocq-verified-extraction
- rocq-yalla
Conflicts
None
On This Page