coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] binary distribution for Leopard (and Snow Leopard), Thorsten Altenkirch
- Re: [Coq-Club] binary distribution for Leopard (and Snow Leopard),
Matthieu Sozeau
- [Coq-Club] what are "levels" in Coq,
Vladimir Voevodsky
- Re: [Coq-Club] what are "levels" in Coq, Adam Chlipala
- Re: [Coq-Club] what are "levels" in Coq, harke
- Re: [Coq-Club] what are "levels" in Coq,
Vladimir Voevodsky
- Re: [Coq-Club] what are "levels" in Coq, Adam Chlipala
- Re: [Coq-Club] what are "levels" in Coq,
Thorsten Altenkirch
- Re: [Coq-Club] what are "levels" in Coq,
Yves Bertot
- Re: [Coq-Club] what are "levels" in Coq, Lionel Elie Mamane
- [Coq-Club] Type hierarchy,
Jean-Francois Dufourd
- Re: [Coq-Club] Type hierarchy, André Hirschowitz
- Re: [Coq-Club] Type hierarchy, Hugo Herbelin
- Re: [Coq-Club] Type hierarchy, Adam Chlipala
- Re: [Coq-Club] Type hierarchy, Hugo Herbelin
- Re: [Coq-Club] what are "levels" in Coq,
Yves Bertot
- Re: [Coq-Club] what are "levels" in Coq,
Vladimir Voevodsky
- [Coq-Club] what are "levels" in Coq,
Vladimir Voevodsky
- Re: [Coq-Club] binary distribution for Leopard (and Snow Leopard),
Matthieu Sozeau
Archive powered by MhonArc 2.6.16.