package coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3.2+coq8.13.tar.gz
sha512=977d343cefbd2d75c180614efe19026fc68d1b8ac35cb0a07267279823e14c9c0632cf2554ff038d73b263fb005b7d0936d9e6d0a601bb19904e92b4ae624d50
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:2021-10-01Published: 01 Oct 2021
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page