package coq-tactician-stdlib
Recompiles Coq's standard libary with Tactician's instrumentation loaded
Install
Dune Dependency
Authors
Maintainers
Sources
1.0-beta1-8.11.tar.gz
sha512=3525285687a023c353170ba611e572fd2051e360c63bf78e8239864409db5a8ee36d876b66bc7cb97248fd0e2f8adbbaa2d189cbe06a2e322734c2ea711a98ad
Description
*** WARNING *** This package will overwrite Coq's standard library files.
This package recompiles Coq's standard library with Tactician's (coq-tactician
)
instrumentation loaded such that Tactician can learn from the library. When you
install this package, the current .vo
files of the standard library are backed
in the folder user-contrib/Tactician/stdlib-backup
. Then exactly the same .vo
files are installed, except that they also contain Tactician's tactic databases.
Upon removal of this package, the original files will be placed back.
Tags
keyword:tactic-learning keyword:machine-learning keyword:automation keyword:proof-synthesis category:Miscellaneous/Coq Extensions logpath:TacticianPublished: 03 Dec 2020
Dependencies (2)
- coq-tactician
-
coq
>= "8.11" & < "8.12~"
Dev Dependencies
None
Used by
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page