package rocq-mathcomp-bigenough
A small library to do epsilon - N reasoning
Install
Dune Dependency
Authors
Maintainers
Sources
1.0.4.tar.gz
sha512=278e4273f55eed9c8267c405198126706d48b0a221f6783b4aa440380ab8453eedbdbad8c65e6338d8043fc51f42027d735214833b8d3ae5d1d09344980f321c
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: 23 Feb 2026
Dependencies (3)
-
rocq-mathcomp-boot
>= "2.5" -
coq-mathcomp-ssreflect
>= "1.6" & <= "2.4" -
coq
>= "8.10" & < "8.21~"
Dev Dependencies (1)
-
rocq-core
>= "9.0" | = "dev"
Used by (1)
-
coq-mathcomp-bigenough
>= "1.0.4"
Conflicts
None
On This Page