ltac2-tutorial
Ltac2 tutorial
A tutorial on Ltac2 tactics language for Coq proof scripting
Ltac2 tutorial
43 stars
8 watching
3 forks
Language: Coq
last commit: about 2 years ago coqltac2
Related projects:
| Repository | Description | Stars |
|---|---|---|
 mtac2/mtac2 | A plugin for Coq that extends its proof assistant with a typed tactic language for backward reasoning. | 51 |
 math-comp/tutorial_material | Tutorials and materials for teaching Coq-based mathematical component development | 17 |
 coq-community/coq-tricks | A resource for discovering useful techniques and tricks in Coq | 507 |
 ptival/haystac | A collection of Ltac tactics to help find specific mathematical proofs in Coq | 5 |
 martinchavez/linq | A test-driven learning project on C# Language Integrated Query (LINQ) concepts and syntax | 61 |
| coq-community/coq-art | Coq proof assistant book with exercises and examples | 114 |
 anton-trunov/coq-lecture-notes | Lecture notes and resources for learning the Coq proof assistant | 50 |
 codyroux/broad-coq-tutorial | Unstructured notes and resources concerning the Broad tutorial in Coq language | 31 |
 plclub/lngen | Tool for generating Coq definitions and proofs for locally nameless representations | 30 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 518 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
 cpitclaudel/alectryon | A tool for processing Coq and Lean 4 code embedded in text documents | 237 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
 pedrotst/coquedille | Translates Coq terms into Cedille terms for a specific domain-specific language | 33 |
| cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 351 |