package coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3-coq8.12.tar.gz
sha512=666ea825c122319e398efb7287f429ebfb5d35611b4cabe4b88732ffb5c265ef348b53d5046c958831ac0b7a759b44ce1ca04220ca68b1915accfd23435b479c
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:2020-07-28Published: 04 Aug 2020
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page