package coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.2-coq8.10.tar.gz
sha512=74b1a014f4e1e62148e25d46a4b2c376b927a3481ef52ce853d43f526164bbffd0bf2184653ba13e638d9321635ceec85e7c7b34e08dfa362c5e7a9588dc4b96
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:2020-04-25Published: 03 Jun 2020
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page