package coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.1.1-coq8.9.tar.gz
sha256=4f167c5fa8cc8a26c81a0efb6f7c360acf4f15151d3d53f8d0c8ab654c8dd814
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-06-12Published: 13 Jun 2019
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page