{"repo":"rocq-community/lemma-overloading","free":true,"listed":false,"github":"https://github.com/rocq-community/lemma-overloading","clone":"git clone https://github.com/rocq-community/lemma-overloading.git","description":"Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]","language":"Rocq Prover","stars":28,"topics":["coq","canonical-structures","typeclasses","ssreflect","mathcomp","automation","paper-artifacts"],"license":null,"category":"workflow-automation","readme_excerpt":"Lemma Overloading [![Docker CI][docker-action-shield]][docker-action-link] [![Contributing][contributing-shield]][contributing-link] [![Code of Conduct][conduct-shield]][conduct-link] [![Zulip][zulip-shield]][zulip-link] [![coqdoc][coqdoc-shield]][coqdoc-link] [![DOI][doi-shield]][doi-link] [docker-action-shield]: https://github.com/coq-community/lemma-overloading/actions/workflows/docker-action.yml/badge.svg?branch=master [docker-action-link]: https://github.com/coq-community/lemma-overloading/actions/workflows/docker-action.yml [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md [conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg [conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE OF CONDUCT.md [zulip-shield]: https://img.shields.io/badge/chat-on%20zulip-%23c1272d.svg [zulip-link]: https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users [coqdoc-shield]: https://img.shields.io/badge/docs-coqdoc-blue.svg [coqdoc-link]: https://coq-community.org/lemma-overloading [doi-shield]: https://zenodo.org/badge/DOI/10.1017/S0956796813000051.svg [doi-link]: https://doi.org/10.1017/S0956796813000051 This project contains Hoare Type Theory libraries which demonstrate a series of design patterns for programming with canonical structures that enable one to carefully and predictab","default_branch":null,"files":null,"tree":[],"storefront":"/r/rocq-community","claimed":false,"request_supported":{"post":"https://gitbuyer.com/r/rocq-community/lemma-overloading/request-supported","requests":0},"note":"indexed from public GitHub; nothing is for sale on this page. Clone it from GitHub. Paid listings live at /search."}