coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Syntax for paraneterized Type Class instances
- Date: Tue, 16 Dec 2014 12:59:11 +0000
- Accept-language: de-DE, en-US
Dear Matthieu,
with your hint I found the section 2.7.20 “Implicit generalization”, which describes this, and when I use an accent grave + space quote + the Generalizable command, it works.
What is rather confusing is that when I cut and paste the code from the reference manual, I get this error:
Syntax Error: Lexer: Undefined token.
Somehow the quote gets messed up during copy and paste. Btw.: The quote used in section 2.7.20 is typographically different from the one in section 19.3, so during preparation of the manual also something seems to go wrong. But for me copy and paste works for neither variant.
Thanks for the help!
Best regards,
Michael
From: matthieu.sozeau AT gmail.com [mailto:matthieu.sozeau AT gmail.com]
On Behalf Of Matthieu Sozeau
Hi Michael,
This prime is a backquote, I think it is described in a section about generalizable variables, or at least the command Generalizable Variables A B which you need here should be in the command index. Didn't you get at least one error saying something close to "unbound and non-generalizable variable A"?
Best,
Dear Coq Users,
|
- [Coq-Club] Syntax for paraneterized Type Class instances, michael.soegtrop, 12/16/2014
- Re: [Coq-Club] Syntax for paraneterized Type Class instances, Matthieu Sozeau, 12/16/2014
- RE: [Coq-Club] Syntax for paraneterized Type Class instances, Soegtrop, Michael, 12/16/2014
- Re: [Coq-Club] Syntax for paraneterized Type Class instances, Matthieu Sozeau, 12/16/2014
Archive powered by MHonArc 2.6.18.