Coqtail

Proof Assistant

Enables interactive proof development in Vim similar to other proof assistants.

Interactive Coq Proofs in Vim

GitHub

274 stars
7 watching
34 forks
Language: Python
last commit: 4 months ago
Linked from 1 awesome list

coqproof-assistantvim

Backlinks from these awesome lists:

Related projects:

Repository Description Stars
ejgallego/pycoq Python bindings for Coq's interactive proof assistant 50
coq/vscoq An extension for Visual Studio Code and VSCodium to support Coq Proof Assistant 349
coq-community/coq-art Coq proof assistant book with exercises and examples 114
coq/platform A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching 191
princeton-vl/coqgym A learning environment for theorem proving with the Coq proof assistant 388
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. 518
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 153
math-comp/coq-combi Formalizes algebraic combinatorics and symmetric functions in Coq. 37
cpitclaudel/company-coq An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software 351
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