package coq-mathcomp-bigenough
A small library to do epsilon - N reasoning
Install
Dune Dependency
Authors
Maintainers
Sources
1.0.2.tar.gz
sha512=faaa56c7db5b00a3e3b1a60dc0b3623d8ef5bcf7d08a228df2184e79a124f9dbd4917b2c24cef0bd9ad98b3dd7aae331d5fbe6dd2d154b80fdc108d8dc828b29
Description
The package contains a package to reasoning with big enough objects
(mostly natural numbers). This package is essentially for backward
compatibility purposes as bigenough will be subsumed by the near
tactics. The formalization is based on the Mathematical Components
library.
Tags
keyword:bigenough keyword:asymptotic reasonning keyword:small scale reflection keyword:mathematical components logpath:mathcomp.bigenoughPublished: 25 Jan 2025
Dependencies (1)
-
coq-mathcomp-ssreflect
>= "1.6"
Dev Dependencies (1)
-
coq
(>= "8.10" & < "9.1~") | (= "dev")
Used by (8)
- coq-hanoi
-
coq-mathcomp-analysis
!= "0.2.3" - coq-mathcomp-apery
- coq-mathcomp-cad
- coq-mathcomp-experimental-reals
-
coq-mathcomp-finmap
>= "1.2.0" & < "1.5.1" -
coq-mathcomp-multinomials
>= "1.1" -
coq-mathcomp-real-closed
>= "1.0.2"
Conflicts
None
On This Page