package coq-mathcomp-zify
Micromega tactics for Mathematical Components
Install
Dune Dependency
Authors
Maintainers
Sources
1.6.0+2.3+8.18.tar.gz
sha256=d15f32d0b9ebef22f6f8bf91cc27390008c9f269ecbddfd6098d3bcb7cedde8b
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.3" & < "2.6~") -
coq
(>= "8.18" & < "9.2~")
Dev Dependencies
None
Used by (6)
-
coq-algorand
>= "1.4" - coq-gaia-hydras
- coq-mathcomp-algebra-tactics
-
coq-mathcomp-apery
>= "1.0.2" -
coq-prosa
>= "0.5" - rocq-prosa
Conflicts
None
On This Page