package coq-mathcomp-zify
Micromega tactics for Mathematical Components
Install
Dune Dependency
Authors
Maintainers
Sources
1.3.0+1.12+8.13.tar.gz
sha256=00a42aae961a5fdc5b3f8b80150065a3401dd188d2f8f42cdcff31520a687578
Description
This small library enables the use of the Micromega arithmetic solvers of Coq for goals stated with the definitions of the Mathematical Components library by extending the zify tactic.
Dependencies (3)
- coq-mathcomp-algebra
-
coq-mathcomp-ssreflect
(>= "1.12" & < "1.20~") -
coq
(>= "8.13" & < "8.21~")
Dev Dependencies
None
Used by (5)
-
coq-algorand
>= "1.4" - coq-gaia-hydras
-
coq-mathcomp-algebra-tactics
< "1.2.0" -
coq-mathcomp-apery
>= "1.0.2" -
coq-prosa
>= "0.5"
Conflicts
None
On This Page