The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

A related question: does Cow has an "internal representation" language  
with a more rigid syntactic structure?

V.




On Oct 6, 2009, at 2:11 PM, 
harke AT cs.pdx.edu
 wrote:

> 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