lemma-overloading
Proof automation library
A Coq library demonstrating design patterns for automated proof automation and canonical structures
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
26 stars
10 watching
6 forks
Language: Coq
last commit: 8 days ago
Linked from 2 awesome lists
automationcanonical-structurescoqmathcomppaper-artifactsssreflecttypeclasses
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| coq-community/coq-art | Coq proof assistant book with exercises and examples | 110 |
| coq-community/autosubst | Automates formalizing syntactic theories with variable binders in Coq | 52 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 66 |
| coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
| coq-community/math-classes | A library of abstract interfaces for various mathematical structures to facilitate algebraic manipulation and type class-based reasoning in Coq | 162 |
| coq-community/topology | Develops and formalizes basic concepts and results of general topology in Coq. | 47 |
| coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 28 |
| coq-community/coqtail-math | A collection of mathematical theorems and tools within the Coq proof assistant | 15 |
 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/alea | A library for reasoning about randomized algorithms in Coq | 25 |
| coq-community/atbr | A Coq library providing algebraic tools and tactics for working with binary relations | 23 |
| coq-community/bits | A formalization of bitset operations in Coq with extraction to OCaml native integers. | 22 |
| coq-community/comp-dec-modal | Machine-checked proofs of soundness, completeness, and decidability for modal logics in Coq. | 8 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |