package coq-tactician-dummy
A dummy implementation of Tactician
Install
Dune Dependency
Authors
Maintainers
Sources
1.0-beta1.tar.gz
sha512=99c2a46202263745fa509a5fcea4b8a09f0cfb5e268a5fa610e32731781a3235845d977e299d3a48c4f2a7b2e3cae0b2b415c7bc57f4b685e8da960a53ac40ca
Description
This package acts as a stand-in for the Tactician plugin (coq-tactician
).
It provides short files that replicate Tactician's tactics without actually
doing much. This is useful when you have a development that uses Tactician
that you want to package up. In most situations, it is not a good idea to
have your package directly depend on coq-tactician
. Instead you should load
Tactician through your coqrc
file. In order for your package to be compilable
by others, your package can depend on this package. Just add
From Tactician import Ltac1Dummy
in your development and you are good to go.
Tags
keyword:tactic-learning keyword:machine-learning keyword:automation keyword:proof-synthesis category:Miscellaneous/Coq Extensions logpath:TacticianPublished: 03 Dec 2020
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page