package coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.1.1-coq8.10.tar.gz
sha512=c9fd9c1a997775f515850fad54edceac6572d365f1e7cc043e448d6e5c9903ccb1bea2020fbbfda3983616f9ae4181a384b933f97731a487ee5cfba7cc1543d1
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 date:2019-10-14Published: 14 Oct 2019
On This Page