package coq-mathcomp-zify
Micromega tactics for Mathematical Components
Install
Dune Dependency
Authors
Maintainers
Sources
1.4.0+2.0+8.16.tar.gz
sha256=913ded0c027837f14004b74ee06f5d4596c22c5695cf688ecd90d6b56509936c
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
(>= "2.0" & < "2.1~") -
coq
(>= "8.16" & < "8.18~")
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