PeaCoq
IDE
A Coq-based IDE with OCaml plugin and TypeScript support
PeaCoq is a pretty Coq, isn't it?
106 stars
8 watching
10 forks
Language: Coq
last commit: over 3 years ago
Linked from 2 awesome lists
uhub/awesome-coq
awesomo4000/awesome-provableRelated projects:
| Repository | Description | Stars |
|---|---|---|
 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 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |
 coq/vscoq | An extension for Visual Studio Code and VSCodium to support Coq Proof Assistant | 349 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 351 |
 lpcic/coq-elpi | Provides an extension language for Coq to manipulate terms containing binders and supports scripting and metaprogramming | 141 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 518 |
| ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 coq-community/paramcoq | A Coq plugin providing commands for generating parametricity statements used in data refinement proofs. | 45 |
 smtcoq/smtcoq | An OCaml-based plugin for Coq that verifies and extends proof witnesses from external SAT/SMT solvers | 157 |
| coq-community/bits | A formalization of bitset operations in Coq with extraction to OCaml native integers. | 22 |
 lysxia/coq-simple-io | Provides tools to implement IO programs directly in Coq | 31 |
| mit-plv/rupicola | A toolkit for compiling functional programs into imperative code for performance-critical applications | 51 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 388 |
 unicoq/unicoq | A plugin for Coq that improves its unification algorithm | 51 |