coq-elpi
Term manipulator
Provides an extension language for Coq to manipulate terms containing binders and supports scripting and metaprogramming
Coq plugin embedding elpi
141 stars
9 watching
52 forks
Language: OCaml
last commit: 10 months ago
Linked from 2 awesome lists
coqextension-languagelambda-prologmetaprogrammingscripting
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 351 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |
 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 |
 plclub/lngen | Tool for generating Coq definitions and proofs for locally nameless representations | 30 |
 coq/vscoq | An extension for Visual Studio Code and VSCodium to support Coq Proof Assistant | 349 |
| coq-community/coq-ext-lib | A collection of reusable Coq definitions and theorems for building software development tools | 129 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
 ptival/peacoq | A Coq-based IDE with OCaml plugin and TypeScript support | 106 |
| plclub/hs-to-coq | A tool that translates Haskell code to equivalent Coq code | 79 |
 lysxia/coq-simple-io | Provides tools to implement IO programs directly in Coq | 31 |
| ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 coq-concurrency/pluto | A Coq-based web server written in a functional programming language | 86 |
 eugeneloy/coq_jupyter | A Jupyter notebook kernel for interactive theorem proving with Coq | 94 |