package coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3.2+8.20.tar.gz
sha512=ec54095d91be602d70c5717f7b9710aca19de8dc02fff97b695aad791912f284438f03c90905ff000ab1e172d1c194cf18ed20f5c33d15edfbd1b85720b38f74
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:2024-11-15Published: 15 Nov 2024
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page