Coqtail
Proof Assistant
Enables interactive proof development in Vim similar to other proof assistants.
Interactive Coq Proofs in Vim
274 stars
7 watching
34 forks
Language: Python
last commit: 2 months ago
Linked from 1 awesome list
coqproof-assistantvim
Related projects:
| Repository | Description | Stars |
|---|---|---|
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 coq/vscoq | A Visual Studio Code extension for Coq proof assistant support | 343 |
 coq-community/coq-art | Coq proof assistant book with exercises and examples | 110 |
| coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 188 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 384 |
 anton-trunov/coq-lecture-notes | Lecture notes and resources for learning the Coq proof assistant | 50 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 515 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
 impermeable/coq-waterproof | Helps write formal proofs in a more readable format | 33 |
| ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 math-comp/coq-combi | Formalises algebraic combinatorics in Coq using symmetric functions and polynomials | 36 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 354 |
 arthuraa/poleiro | A blog about Coq proof assistant and its related libraries and tools | 47 |
 eugeneloy/coq_jupyter | A Jupyter notebook kernel for interactive theorem proving with Coq | 94 |