package coq-coquelicot
A Coq formalization of real analysis compatible with the standard library
Install
Dune Dependency
Authors
Maintainers
Sources
coquelicot-3.4.4.tar.gz
sha512=d0e4bddb4438b9750458ea160a3051b421384ba524675c870183aa5061b3294dd347093fefd0682f04af2d4a5086e5911dfed39f9df7f6188caca3082a9f205c
Description
Tags
keyword:real analysis keyword:topology keyword:filters keyword:metric spaces category:Mathematics/Real Calculus and Topology logpath:Coquelicot date:2025-07-30Published: 30 Jul 2025
Dependencies (4)
-
conf-clang
build -
conf-g++
build -
coq-mathcomp-ssreflect
>= "1.6" -
coq
>= "8.12"
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