coq-art
Proof assistant
Coq proof assistant book with exercises and examples
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
114 stars
7 watching
22 forks
Language: Coq
last commit: 7 months ago
Linked from 2 awesome lists
coqcoq-artdocker-coq-actionexercises
Related projects:
Repository | Description | Stars |
---|---|---|
| Provides pre-configured Docker images for building and testing the Coq proof assistant | 37 |
| Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
| An extension for Visual Studio Code and VSCodium to support Coq Proof Assistant | 349 |
| A resource for discovering useful techniques and tricks in Coq | 507 |
| A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 191 |
| A Coq implementation of the Japanese warehouse keeper's puzzle game Sokoban | 21 |
| Repository tracking famous theorems proved using proof assistants. | 57 |
| A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 30 |
| A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
| A Coq library providing algebraic data structures and algorithms | 67 |
| A collection of reusable Coq definitions and theorems for building software development tools | 129 |
| Enables interactive proof development in Vim similar to other proof assistants. | 274 |
| Tutorials and materials for teaching Coq-based mathematical component development | 17 |
| Provides Docker images for a Coq proof assistant library | 6 |
| Python bindings for Coq's interactive proof assistant | 50 |