package coq-mathcomp-zify

  1. Overview
  2. Homepage
Micromega tactics for Mathematical Components

Install

Dune Dependency

Authors

Maintainers

Sources

1.3.0+1.12+8.13.tar.gz
sha256=00a42aae961a5fdc5b3f8b80150065a3401dd188d2f8f42cdcff31520a687578

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.

Tags

logpath:mathcomp.zify

Published: 14 Feb 2023

Dependencies (3)

  1. coq-mathcomp-algebra
  2. coq-mathcomp-ssreflect (>= "1.12" & < "1.20~")
  3. coq (>= "8.13" & < "8.21~")

Dev Dependencies

None

Conflicts

None

Rocq

Interactive Theorem Prover