coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: zell08v AT orange.fr
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Built-in syntactic equality ?
Date: Tue, 2 Mar 2010 17:54:53 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=thaFzNtj8y8kHFeR7z+9gQ3PpX0/IHBCRmJ75SAYZU7DZg8qO9fpJcDVxqNtjfXcuX qkmpU2DDLvyKyaQ/2ZKRS9ol46MbQxBQWfgaPhbNttPn+ukSXl4/0efdNN8CLyHLp3Jy /4uzpbOgbcypaHA9U2YSV+JUJ2UcEA/fPW+eE=

��Dear Z,

��See Chapter 9 of Adam Chlipala's book about Coq for an in-depth treatment of equality in Coq.

��Best,

��(another) Adam

--
Adam Koprowski � [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate � �[http://mlstate.com, 15 rue Berlier, 75013 Paris, France]

[Coq-Club] Built-in syntactic equality ?, zell08v
- Re: [Coq-Club] Built-in syntactic equality ?, Adam Koprowski
- Re: [Coq-Club] Built-in syntactic equality ?, Matthieu Sozeau