The Coq mailing list

[harke AT cs.pdx.edu]

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