package coq-hammer

You can search for identifiers within the package.

in-package search v0.2.0

General-purpose automated reasoning hammer tool for Coq

Install

Dune Dependency

github.com Edit opam file Versions (34)

Authors

Maintainers

L

lukaszcz@mimuw.edu.pl

Sources

v1.3.3+9.2.tar.gz

sha512=6547d6824795a7f3d0281c0931be2c63571443a28df7467dfe7caa0380845653a3f1a61c71550ff3bd64c18b2694336c2e04a412e65ea9bddcdb3d2b5aa940d9

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.

Published: 09 Jul 2026

Dependencies (6)

coq-hammer-tactics = version
conf-clang build
conf-g++ build
rocq-stdlib >= "9.1" & < "9.3~"
rocq-core >= "9.2" & < "9.3~"
ocaml >= "4.09"

Dev Dependencies

None

Used by (1)

coq-operads

Conflicts