extructures
Equality library
Provides data structures and reasoning tools for extensional equality in Coq
Finite sets and maps for Coq with extensional equality
29 stars
2 watching
6 forks
Language: Coq
last commit: about 1 year ago coqfinite-setsmathcompssreflect
Related projects:
| Repository | Description | Stars |
|---|---|---|
 llee454/functional-algebra | A Coq formalization of abstract algebra using functional programming style | 28 |
 coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 66 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
| coq-community/atbr | A Coq library providing algebraic tools and tactics for working with binary relations | 23 |
| coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 28 |
 geocoq/geocoq | A formalization of geometry using the Coq proof assistant. | 186 |
| arthuraa/deriving | Automatically generates boilerplate code for Coq inductive types | 24 |
| coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
 vafeiadis/hahn | A collection of lemmas and tactics about lists and binary relations for a proof assistant | 30 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
| arthuraa/poleiro | A blog about Coq proof assistant and its related libraries and tools | 47 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
| coq-community/dedekind-reals | A formalization of Dedekind reals numbers in the Coq programming language | 43 |
| coq-community/coqtail-math | A collection of mathematical theorems and tools within the Coq proof assistant | 15 |
| coq-community/hydra-battles | Investigating various aspects of discrete mathematics and formal proofs in Coq, including ordinal numbers and computability theory. | 68 |