package coq-hammer-tactics

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

Install

Dune Dependency

Authors

Maintainers

Sources

v1.3.2+coq8.14.tar.gz
sha512=68c6e6a2054ce9dd3d87cb61e667f638e7b9fb2b5ec9571427d9fac59d0901cbfa4e57c59edb3a8bc52c2626985fca6edbac42caf2acdc5858fb6e13f15afcea

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.14" & < "8.15~"
  2. ocaml >= "4.08"

Dev Dependencies

None

Used by (1)

  1. coq-hammer = "1.3.2+8.14"

Conflicts (1)

  1. coq-hammer != version
Rocq

Interactive Theorem Prover