package coq-hammer
General-purpose automated reasoning hammer tool for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.1.1-coq8.9.tar.gz
sha256=4f167c5fa8cc8a26c81a0efb6f7c360acf4f15151d3d53f8d0c8ab654c8dd814
Description
A general-purpose automated reasoning hammer tool for Coq that combines learning from previous proofs with the translation of problems to the logics of automated systems and the reconstruction of successfully found proofs.
Tags
category:Miscellaneous/Coq Extensions keyword:automation keyword:hammer logpath:Hammer date:2019-06-12Published: 13 Jun 2019
Dependencies (4)
-
coq-hammer-tactics
= version
-
conf-g++
build
-
coq
>= "8.8" & < "8.10~"
- ocaml
Dev Dependencies
None
Used by
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page