Lemma Overloading

NOASSERTIONRocq Proverv8.12.0

Libraries demonstrating design patterns for programming and proving with canonical structures in Coq's Hoare Type Theory.

28 stars6 forks0 contributors

Overview

Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]

Community-curated · Updated weekly · 100% open source

Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.

Last commit

4 months ago

CreatedSince 2016

Auto-fetched 1 day ago

Tricks you wish the Coq manual told you [maintainer=@tchajed]

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

proof script associated to tutorial material

Whirlwind tour of Coq as a language