package coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3.1-coq8.11.tar.gz
sha512=5e5d01b0f2b19268b038e89cebd41103442987cd11a81b6b615553167444f2081e92bebd483e464ff3d47f080784f1104858ad170fc188124a066b55a1fea722
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-05-20Published: 07 Jun 2021
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page