package coq-mathcomp-zify

You can search for identifiers within the package.

in-package search v0.2.0

Micromega tactics for Mathematical Components

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

K

Kazuhiko Sakaguchi

Maintainers

K

kazuhiko.sakaguchi@inria.fr

Sources

1.1.0+1.12+8.13.tar.gz

sha256=0b650960a5d6b708f6224e8946297ced8f042169c2e3c36c34c4fb38dcfb462e

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.

Published: 30 Sep 2021

Dependencies (3)

coq-mathcomp-algebra
coq-mathcomp-ssreflect (>= "1.12" & < "1.17~")
coq (>= "8.13" & < "8.17~")

Dev Dependencies

None

Used by (3)

coq-algorand >= "1.4"
coq-gaia-hydras
coq-mathcomp-algebra-tactics < "1.2.0"

Conflicts