Tactician
Interactive tool which learns from previously written tactic scripts across all the installed Coq packages and suggests the next tactic to be executed or tries to automate proof synthesis fully.
- from
- Coq
- added
- 2026-10-10
- likes
- 0
similar
-
Coq Tactics in Plain English charlesaverill.github.io
Guide to Coq tactics with explanations and examples.
-
Ltac2 coq.inria.fr
Experimental typed tactic language similar to Coq's classic Ltac language.
-
coq-tools github.com
Scripts for manipulating Coq developments.
-
Tricks in Coq github.com
Tips, tricks, and features in Coq that are hard to discover.
-
Coq'Art Exercises and Tutorials github.com
Coq code and exercises from the Coq'Art book, including additional tutorials.
-
CoqIDE coq.inria.fr
Standalone graphical tool for interacting with Coq.
Coq › Projects > Plugins: “Interactive tool which learns from previously written tactic scripts across all the installed Coq packages and suggests the next tactic to be executed or tries to automate proof synthesis fully.”