coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Canonical Structure

From: Vladimir Komendantsky <vk AT cs.st-andrews.ac.uk>
To: coq-club AT inria.fr
Subject: [Coq-Club] Canonical Structure
Date: Thu, 18 Mar 2010 11:37:49 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; b=EgEL1AcWb9s+ic/cp7huOPAa16veWLbDuZJbuUdtzQxrq2tZFfTSuZkrUFbyDHQjd+ P1AKsYs3YZwmVOUgiRviX2FfCKRY+ZlrBEzHjtLQYUU1bnQJc62Hif8z+OtsGSl92Rrd jSMN3ZC2SAW995TeMjheA/nnhitlWqm2NQPEI=

Hello,

It would be interesting to know whether Canonical Structure has a
formal representation in the CiC. The reference manual describes it as
a type-checker hint. However, canonical structures are complementary
related to implicit coercions that seem to be representable in the
CiC.

Is there a reference on the implementation of canonical structures?

Regards,
Vladimir

[Coq-Club] Canonical Structure, Vladimir Komendantsky
- RE: [Coq-Club] Canonical Structure, Georges Gonthier