coq-art
Proof assistant
Coq proof assistant book with exercises and examples
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
110 stars
7 watching
22 forks
Language: Coq
last commit: 4 months ago
Linked from 2 awesome lists
coqcoq-artdocker-coq-actionexercises
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| coq-community/docker-coq | Provides pre-configured Docker images for building and testing the Coq proof assistant | 37 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
 coq/vscoq | A Visual Studio Code extension for Coq proof assistant support | 343 |
| coq-community/coq-tricks | A resource for discovering useful techniques and tricks in Coq | 503 |
| 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/coqoban | A Coq implementation of the Japanese warehouse keeper's puzzle game Sokoban | 21 |
| coq-community/coq-100-theorems | Repository tracking famous theorems proved using proof assistants. | 55 |
| coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 28 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 66 |
| coq-community/coq-ext-lib | A collection of reusable Coq definitions and theorems for building software development tools | 129 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 math-comp/tutorial_material | Tutorials and materials for teaching Coq-based mathematical component development | 17 |
| math-comp/docker-mathcomp | Provides Docker images for a Coq proof assistant library | 6 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |