package coq-mathcomp-bigenough
A small library to do epsilon - N reasoning
Install
Dune Dependency
Authors
Maintainers
Sources
1.0.3.tar.gz
sha512=8bbe849e4e6331bfed0eacb2e8f7042fb4aedd280232987be5932e9a044be8685b0c9e7136fe07ee80b5918fb8d914ccb9d391ef03b9fffbe8f162bc787e7ef7
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: 13 Nov 2025
Dependencies (1)
-
coq-mathcomp-ssreflect
>= "1.6"
Dev Dependencies (1)
-
coq
(>= "8.10" & < "9.2~") | (= "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