package coq-tactician-dummy
A dummy implementation of Tactician
Install
Dune Dependency
Authors
Maintainers
Sources
1.0-beta2-8.11.tar.gz
sha512=89aa13aff38e7ff3d53c00c0a604771ee1b3d0fadb3dab21161b28e25ab9fa14bd834a445472c05140c881ba7b7205ed81ca20b479002573051f42660428e9bb
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 Require 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: 19 Oct 2023
Dev Dependencies
None
Used by (1)
-
coq-tactician
>= "1.0~beta2~neural+8.11" & < "1.0~beta2.1+8.17"
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page