package coq-coquelicot
A Coq formalization of real analysis compatible with the standard library
Install
Dune Dependency
Authors
Maintainers
Sources
coquelicot-3.4.5.tar.gz
sha512=6a94f674715175347ff9938f8ac0f6e865c0019e6b6317d292e4c9d7e30df7ebd41dfe48205a61f66c0bde0da1702d9831161439189dbc8337524d51f05e1a99
Description
Tags
keyword:real analysis keyword:topology keyword:filters keyword:metric spaces category:Mathematics/Real Calculus and Topology logpath:Coquelicot date:2026-08-27Published: 27 Aug 2026
Dependencies (8)
-
conf-clang
build -
conf-g++
build -
ocaml
build -
coq-mathcomp-ssreflect
>= "1.6" - rocq-stdlib
- coq-stdlib
- coq-core
-
coq
>= "8.12" & < "8.17~"
Dev Dependencies (1)
-
conf-autoconf
build & dev
Used by (10)
- coq-actuary
- coq-approx-models
- coq-improper-integrals
-
coq-interval
>= "3.2.0" -
coq-libvalidsdp
>= "0.6.0" -
coq-pi-agm
>= "1.2.0" -
coq-plouffe
= "1.1.0" | >= "1.3.0" - rocq-num-analysis-algebra
- rocq-num-analysis-lebesgue
- rocq-pi-agm
Conflicts
None
On This Page