package coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3.2+coq8.15.tar.gz
sha512=0277150c2fd570400693ee1a3e4b2f253fbf7cc4b9997a803bb5e0e3e633352eb8cca2f3e8b1c47e49b9994b73c6f744f31e9e81eac665d1bf7ed4054ef39512
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.
Tags
keyword:automation keyword:hammer keyword:tactics logpath:Hammer.Tactics date:2022-01-23Published: 23 Jan 2022
On This Page