package coq-mathcomp-zify
Micromega tactics for Mathematical Components
Install
Dune Dependency
Authors
Maintainers
Sources
1.5.0+2.0+8.16.tar.gz
sha256=5988389c6c8dfde4d2f3a370278c6b2aa1b5a0f56531cb30b0cce2d550b4387c
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.4~") -
coq
(>= "8.16" & < "9.1~")
Dev Dependencies
None
Used by (5)
-
coq-algorand
>= "1.4" - coq-gaia-hydras
- coq-mathcomp-algebra-tactics
-
coq-mathcomp-apery
>= "1.0.2" -
coq-prosa
>= "0.5"
Conflicts
None
On This Page