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