package coq-tactician-stdlib
Recompiles Coq's standard libary with Tactician's instrumentation loaded
Install
Dune Dependency
Authors
Maintainers
Sources
1.0-beta1-8.12.tar.gz
sha512=a5a24c47eb8b28663a790cf3a935d7ccc59a856777d659be5b9ad2ef17a793c10a5c824a46fb52627eaf09eb07f553f4e0c16a58ffdec7eb53a9b5908e146f41
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.12" & < "8.13~"
Dev Dependencies
None
Used by
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page