package coq-hammer-tactics

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

Install

Dune Dependency

Authors

Maintainers

Sources

v1.3.2+9.0.tar.gz
sha512=2d105d5c229e573841bbc194ca4eb9a688a9f11a38c409f4b6f9a8fd2675a150c72d210f21f05e0fed441013980be0e5d8f22311565d098afe3d479938e811d5

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 >= "9.0" & < "9.1~"
  2. ocaml >= "4.09"

Dev Dependencies

None

Used by (1)

  1. coq-hammer >= "1.3.2+9.0"

Conflicts (1)

  1. coq-hammer != version
Rocq

Interactive Theorem Prover