package coq-hammer-tactics

  1. Overview
  2. Homepage
Reconstruction tactics for the hammer for Coq

Install

Dune Dependency

Authors

Maintainers

Sources

v1.3-coq8.12.tar.gz
sha512=666ea825c122319e398efb7287f429ebfb5d35611b4cabe4b88732ffb5c265ef348b53d5046c958831ac0b7a759b44ce1ca04220ca68b1915accfd23435b479c

Description

Collection of tactics that are used by the hammer for Coq to reconstruct proofs found by automated theorem provers. When the hammer has been successfully applied to a project, only this package needs to be installed; the hammer plugin is not required.

Dependencies (2)

  1. coq >= "8.12" & < "8.13~"
  2. ocaml

Dev Dependencies

None

Used by (1)

  1. coq-hammer = "1.3+8.12"

Conflicts (1)

  1. coq-hammer != version
Rocq

Interactive Theorem Prover