package coq-hammer

  1. Overview
  2. Homepage
General-purpose automated reasoning hammer tool for Coq

Install

Dune Dependency

Authors

Maintainers

Sources

v1.1.1-coq8.9.tar.gz
sha256=4f167c5fa8cc8a26c81a0efb6f7c360acf4f15151d3d53f8d0c8ab654c8dd814

Description

A general-purpose automated reasoning hammer tool for Coq that combines learning from previous proofs with the translation of problems to the logics of automated systems and the reconstruction of successfully found proofs.

Dependencies (4)

  1. coq-hammer-tactics = version
  2. conf-g++ build
  3. coq >= "8.8" & < "8.10~"
  4. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover