company-coq
Coq IDE
An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software
A Coq IDE build on top of Proof General's Coq mode
354 stars
10 watching
29 forks
Language: Emacs Lisp
last commit: almost 2 years ago
Linked from 1 awesome list
company-modecoqemacsintegrated-development-environmentproof-assistantproof-general
Related projects:
| Repository | Description | Stars |
|---|---|---|
| cpitclaudel/alectryon | Tools for processing Coq code and prose in technical documents | 236 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 515 |
 lpcic/coq-elpi | A Coq plugin embedding Elpi to extend Coq's capabilities with a dialect of lambda-prolog for metaprogramming and scripting. | 139 |
 coq/vscoq | A Visual Studio Code extension for Coq proof assistant support | 343 |
 coq-community/docker-coq | Provides pre-configured Docker images for building and testing the Coq proof assistant | 37 |
| coq-community/paramcoq | A Coq plugin providing commands for generating parametricity statements used in data refinement proofs. | 44 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 41 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 384 |
| coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 188 |
| coq-community/coq-art | Coq proof assistant book with exercises and examples | 110 |
| coq-community/coq-ext-lib | A collection of reusable Coq definitions and theorems for building software development tools | 129 |
 math-comp/docker-mathcomp | Provides Docker images for a Coq proof assistant library | 6 |