package rocq-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 (1)

Authors

K

Kazuhiko Sakaguchi

Maintainers

K

kazuhiko.sakaguchi@inria.fr

Sources

1.7.0+2.4+9.0.tar.gz

sha256=649fa3d82be1cc606261e25b6fd26ddc5b55b2e6697a314b20f0564273089a54

Description

This small library enables the use of the Micromega arithmetic solvers of Rocq for goals stated with the definitions of the Mathematical Components library by extending the zify tactic.

Published: 28 Aug 2026

Dependencies (4)

rocq-mathcomp-algebra
rocq-mathcomp-ssreflect >= "2.4" & < "2.7~"
rocq-stdlib
rocq-core >= "9.0" & < "9.4~"

Dev Dependencies

None

Used by (1)

coq-mathcomp-zify >= "1.7.0+2.4+9.0"

Conflicts