coq-waterproof
Proof writer
Helps write formal proofs in a more readable format
The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.
33 stars
3 watching
11 forks
Language: Coq
last commit: 3 months ago
Linked from 1 awesome list
Related projects:
| Repository | Description | Stars |
|---|---|---|
| impermeable/waterproof | An interactive notebook environment for writing and proving mathematical proofs in a logical language | 40 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 math-comp/coq-combi | Formalizes algebraic combinatorics and symmetric functions in Coq. | 37 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 292 |
 coq-community/coq-art | Coq proof assistant book with exercises and examples | 114 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 518 |
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
| formal-land/coq-of-rust | Tool that verifies Rust code by translating it into Coq's proof system to ensure no bugs or vulnerabilities exist | 437 |
| math-comp/tutorial_material | Tutorials and materials for teaching Coq-based mathematical component development | 17 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 388 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 351 |