package coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3-coq8.11.tar.gz
sha512=f50e39145b772c38cc19b1be7d1d66bd3b1bee6cb685ea897165eaa89fa0b5a746e4ec97a774429ccf2cf9bd10d272331d1b4e2a4b9247080df4ef7fb9600a1d
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