Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] Syntax for paraneterized Type Class instances

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Syntax for paraneterized Type Class instances


Chronological Thread 
  • 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
Sent: Tuesday, December 16, 2014 12:39 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Syntax for paraneterized Type Class instances

 

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,
-- Matthieu


Le mardi 16 décembre 2014, <michael.soegtrop AT intel.com> a écrit :

Dear Coq Users,

I don't understand the syntax given in chapter 19.3 of the reference manual:

Instance prod_eqb ‘(EA : EqDec A, EB : EqDec B) : EqDec (A * B)

What is the meaning of the prime here? Is this an abbreviation for this:

Instance prod_eqb {A B : Type} (EA : EqDec A) (EB : EqDec B) : EqDec (A * B)

Also I have problems to make Coq parse the syntax given in the manual with all
3 prime variants on my keyboard (`'´) and the prime used in the manual (‘).
Is there a description for this syntax in the reference manual?

Thanks & Best regards,

Michael



--




Archive powered by MHonArc 2.6.18.

Top of Page