coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Associativity for free!

From: David Leduc <david.leduc6 AT googlemail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Associativity for free!
Date: Mon, 7 Nov 2011 13:11:36 +0000

A few days ago, on the Agda mailing-list there was a mail by Alan
Jeffrey "about a trick for representing lists (or any other monoid) up
to associativity". It sounds great but unfortunately I cannot speak
Agda. Can anyone translate this mail into Coq? TIA.

https://lists.chalmers.se/pipermail/agda/2011/003420.html

[Coq-Club] Associativity for free!, David Leduc
- Re: [Coq-Club] Associativity for free!, Adam Chlipala
  - Re: [Coq-Club] Associativity for free!, Arnaud Spiwack
    - Re: [Coq-Club] Associativity for free!, Daniel Schepler