package coq-coquelicot
(patched for Coq 8.11 compatibility by MSoegtropIMC) A Coq formalization of real analysis compatible with the standard library
Install
Dune Dependency
Authors
Maintainers
Sources
1ec80657ce992fc5aa660dca86d423671f02e33c.tar.gz
sha512=c164168d3732ff9f0067e95997d6478be497244380a297ac8c092ebefa2d369246f4f8a1e6ae7d5ec6fd32e73f3b9cf96addd067b80b5bc67f3883e0933a3ce2
Description
Tags
keyword:real analysis keyword:topology keyword:filters keyword:metric spaces category:Mathematics/Real Calculus and Topology date:2020-01-14 logpath:CoquelicotPublished: 11 Mar 2020
Dependencies (5)
-
conf-autoconf
build -
conf-clang
build -
conf-g++
build -
coq-mathcomp-ssreflect
>= "1.6" -
coq
= "8.11.0"
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