package coq-mathcomp-reals
A library for real numbers for mathematical components
Install
Dune Dependency
Authors
Maintainers
Sources
analysis-1.10.0.tar.gz
sha512=7be39db1aca5a3c49b2d38167bc1c55c35b64fbe0de69ab22181228aee0366fe039cda21446802d5f8def0190d9bef3fbd9dc0c616505c0c6345372cc94b9ce7
Description
This package contains a library for real numbers for the Coq proof-assistant and using the Mathematical Components library.
Tags
category:Mathematics/Real Numbers keyword:real numbers keyword:reals keyword:extended real numbers logpath:mathcomp.realsPublished: 22 Apr 2025
Dependencies (4)
-
coq-mathcomp-classical
= version -
coq-core
>= "9.0" -
coq-mathcomp-ssreflect
< "2.4~" -
coq
< "8.21~"
Dev Dependencies
None
Used by (3)
-
coq-mathcomp-analysis
= "1.10.0" -
coq-mathcomp-experimental-reals
= "1.10.0" -
coq-mathcomp-reals-stdlib
= "1.10.0"
Conflicts
None
On This Page