package coq-lemma-overloading

  1. Overview
  2. No Docs
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq

Install

Dune Dependency

github.com Edit opam file Versions (5)

Authors

  1. G
    Georges Gonthier
  2. B
    Beta Ziliani
  3. A
    Aleksandar Nanevski
  4. D
    Derek Dreyer

Maintainers

  1. A
    anton.a.trunov@gmail.com

Sources

v8.12.0.tar.gz
sha512=63a6aa43ef50d5e5e2ea5f9a478c1ed90b37c59b192e89091a66dec36e0a7b5c63abc63daf03939d9afcb7522b26ac434341e90b82fcfd802c8d75787c5082b5

Description

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 predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and illustrates these patterns through several realistic examples drawn from Hoare Type Theory. The project also contains typeclass-based re-implementations for comparison.

Tags

category:Computer Science/Data Types and Data Structures keyword:canonical structures keyword:proof automation keyword:Hoare type theory keyword:lemma overloading logpath:LemmaOverloading date:2020-08-12

Published: 13 Aug 2020

Dependencies

None

Dev Dependencies (2)

  1. coq-mathcomp-ssreflect (>= "1.7" & < "1.12~") | (= "dev")
  2. coq (>= "8.10" & < "8.13~") | (= "dev")

Used by

None

Conflicts

None