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
351 stars
10 watching
28 forks
Language: Emacs Lisp
last commit: about 2 years ago
Linked from 1 awesome list
company-modecoqemacsintegrated-development-environmentproof-assistantproof-general
Related projects:
| Repository | Description | Stars |
|---|---|---|
| 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 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 518 |
 lpcic/coq-elpi | Provides an extension language for Coq to manipulate terms containing binders and supports scripting and metaprogramming | 141 |
 coq/vscoq | An extension for Visual Studio Code and VSCodium to support Coq Proof Assistant | 349 |
 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. | 45 |
| 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 | 42 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 388 |
| coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 191 |
| coq-community/coq-art | Coq proof assistant book with exercises and examples | 114 |
| 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 |