Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] what are "levels" in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] what are "levels" in Coq


chronological Thread 
  • From: harke AT cs.pdx.edu
  • To: Vladimir Voevodsky <vladimir AT ias.edu>
  • Cc: Coq Club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] what are "levels" in Coq
  • Date: Tue, 6 Oct 2009 11:11:20 -0700
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

This is a standard trick for reducing the amount of parenthesisation
used by many languages that have user defined infix operators.

You'll also notice the line:

  Reserved Notation "x /\ y" (at level 80, right associativity).

Try the following in coqide/proofgeneral:

  Variables A B C : Prop.
  Check A /\ (B <-> C).
  Check (A /\ B) <-> C.

You'll see the printout of the first shows parentheses while the second
omits them.  This is due to the different levels.  Then try:
        
  Check (A /\ B) /\ C.
  Check A /\ (B /\ C).

Again, the first shows parens, the second omits, due to the right
associativity.

On Tue, Oct 06, 2009 at 01:52:21PM -0400, Vladimir Voevodsky wrote:
> Hi,
>
>
> I am trying to understand the way in which Coq treats input texts. To  
> some extent it is explained in the first part of the reference manual,  
> but I could not find the explanation for what "levels" are (e.g. in
>
>
> Reserved Notation "x <-> y" (at level 95, no associativity).
>
> from the Coq standard library,)
>
> Also, is there a way to search the reference manual?
>
> Thanks,
> Vladimir.

-- 
Tom Harke





Archive powered by MhonArc 2.6.16.

Top of Page