package coq-coquelicot
A Coq formalization of real analysis compatible with the standard library
Install
Dune Dependency
Authors
Maintainers
Sources
coquelicot-3.0.2.tar.gz
md5=3236249967dd36ca832dd10d1bddcd71
Description
Tags
keyword:real analysis keyword:topology keyword:filters keyword:metric spaces category:Mathematics/Real Calculus and TopologyPublished: 09 May 2018
Dependencies (2)
-
coq-mathcomp-ssreflect
>= "1.6" -
coq
>= "8.5" & < "8.10~"
Dev Dependencies
None
Used by (6)
- coq-improper-integrals
-
coq-interval
>= "3.2.0" & < "4.11.1" -
coq-libvalidsdp
>= "0.6.0" -
coq-pi-agm
>= "1.2.0" -
coq-plouffe
= "1.1.0" | >= "1.3.0" & < "1.5.0" - rocq-pi-agm
Conflicts
None
On This Page