package coq-mathcomp-zify
Micromega tactics for Mathematical Components
Install
Dune Dependency
Authors
Maintainers
Sources
1.2.0+1.12+8.13.tar.gz
sha256=a19515dcfb2a3ec95261b400dbd1bfb820ce6029b8a76d295ab2448e18825958
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.17~") -
coq
(>= "8.13" & < "8.17~")
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