package rocq-stdlib
The Rocq Proof Assistant -- Standard Library
Install
Dune Dependency
Authors
Maintainers
Sources
stdlib-9.2.0.tar.gz
sha512=9160776b4e3097a10008a469752c1459d35298fca2b78c61fdbe023ca41085b4bb88cdc12c77f5dae1166bf6b74671f0afe415ff58f6f102bea716361d52755a
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: 27 Jul 2026
Dependencies (2)
-
rocq-core
>= "9.1" & < "9.4~" - rocq-runtime
Dev Dependencies
None
Used by (66)
-
coq-autosubst
>= "1.10" -
coq-coquelicot
>= "3.4.5" -
coq-coqutil
>= "0.0.7" -
coq-ext-lib
>= "0.13.0" & < "0.13.2" -
coq-fcsl-pcm
>= "2.3.0" -
coq-flocq
>= "4.2.2" -
coq-hammer
>= "1.3.3+9.2" -
coq-hammer-tactics
>= "1.3.3+9.2" -
coq-htt
>= "2.3.0" -
coq-htt-core
>= "2.3.0" -
coq-interval
>= "4.11.4" -
coq-kruskal-almostfull
>= "2.0" -
coq-kruskal-finite
>= "2.0" -
coq-kruskal-trees
>= "2.0" -
coq-ordinal
>= "0.5.6" -
coq-paco
>= "4.2.3" -
coq-record-update
>= "0.3.4" - coq-sflib
-
coq-stdlib
>= "9.2.0" -
coq-vcfloat
>= "2.4.2" -
coq-vst
= "2.17" - rocq-aac-tactics
- rocq-bignums
- rocq-categories
- rocq-coinduction
- rocq-coqprime
- rocq-elpi
- rocq-equations
- rocq-iris
- rocq-jsast
- rocq-laproof
- rocq-lean-import
- rocq-libhyps
- rocq-linux-process-semantics-common
- rocq-linux-process-semantics-core
- rocq-linux-process-semantics-examples
- rocq-listz
- rocq-marble
-
rocq-mathcomp-reals-stdlib
>= "1.18.0" - rocq-mathcomp-zify
- 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-partial
- rocq-partial-orders
- rocq-pi-agm
- rocq-pi-leibniz
- rocq-print-assumptions-json
- rocq-read-file
- rocq-relation-algebra
-
rocq-robot-rocq
>= "0.3.3" - rocq-robust-geometric-predicates
- rocq-semantics
- rocq-smt-lib
- rocq-spatial-algebra
- rocq-stdpp
- rocq-sulfur
- rocq-taylor-rocqs
- rocq-verified-extraction
- rocq-yalla
- strict-order-solver
Conflicts
None
On This Page