coq-community / coq-100-theorems
Statements of famous theorems proven in Coq [maintainer=@jmadiot]
☆57Updated 10 months ago
Alternatives and similar repositories for coq-100-theorems:
Users that are interested in coq-100-theorems are comparing it to the libraries listed below
- Hoare Type Theory☆70Updated last week
- General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]☆47Updated 3 months ago
- Monadic effects and equational reasonig in Coq☆71Updated 3 weeks ago
- Coq plugin embedding elpi☆142Updated this week
- Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]☆115Updated 6 months ago
- Graph Theory [maintainers=@chdoc,@damien-pous]☆34Updated 2 months ago
- A formalisation of the Calculus of Constructions☆66Updated 6 months ago
- A Verified Compiler for Gallina, Written in Gallina☆140Updated this week
- A library of mechanised undecidability proofs in the Coq proof assistant.☆112Updated this week
- ☆28Updated last year
- Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]☆112Updated this week
- A quick reference for mapping Coq tactics to Lean tactics☆69Updated 3 years ago
- An extension to PUMPKIN PATCH with support for proof repair across type equivalences.☆49Updated 4 months ago
- The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]☆67Updated this week
- Yet another plugin tutorial, this time as an exercise for 598☆38Updated last year
- Coq development for the course "Mechanized semantics", Collège de France, 2019-2020☆64Updated 9 months ago
- Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintaine…☆70Updated last week
- An encoding of Zermelo-Fraenkel Set Theory in Coq☆23Updated 2 years ago
- A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]☆163Updated 2 months ago
- High level commands to declare a hierarchy based on packed classes☆97Updated this week
- Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker☆51Updated 6 months ago
- LeanSSR: an SSReflect-Like Tactic Language for Lean☆32Updated 4 months ago
- HoTT in Lean 3☆77Updated 4 years ago
- Archive for all Coq related OPAM packages organized in various repositories☆133Updated this week
- Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]☆54Updated 4 months ago
- Finite sets, finite maps, multisets and generic sets☆47Updated 2 weeks ago
- An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logt…☆139Updated 3 months ago
- LaTeX code for a paper on lean's type theory☆127Updated 2 years ago
- Coq library for verified low-level programming☆57Updated 7 years ago
- A (formalised) general definition of type theories☆57Updated 3 years ago