coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
- To: Gregory Bush <gbush AT mysck.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Notation Question
- Date: Thu, 20 Dec 2012 20:59:19 +0100
Hi,
If you do "Print Grammar constr", you will see that the notation for
sigT follow the following rule:
...
| "0" LEFTA
[ "{"; constr:operconstr LEVEL "99"; ":"; constr:operconstr LEVEL "200";
"&"; constr:operconstr LEVEL "200"; "&"; constr:operconstr LEVEL "200";
"}"
...
Because the underlying parser of Coq, which is camlp4/camlp5, is
basically an LL parser, rules have to be factorized by hand.
To get this factorization, you need to put any notation starting with
"{" at level 0, and with first expression being parsed at level
99. This gives:
Notation "{ A , .. , B }" := (cons A .. (cons B nil) ..) (at level 0, A at
level 99).
This will not hide the notation for sigT but this will break the
notation sumbool though, because "{ A } + { B }" will not be parsed
any longer as a sumbool but as some "+" of singleton lists "{A}" and
"{B}". So maybe, you would prefer to use the notation:
Notation "{ A , B , .. , C }" := (cons A (cons B .. (cons C nil) ..)) (at
level 0, A at level 99).
and to write differently the lists of one element.
Note that it might be wise to set the parsing level for B at 99 too,
depending on whether interferences are likely to happen with other
notations involving ",".
Hope this helps.
Hugo Herbelin
On Thu, Dec 20, 2012 at 02:29:56PM -0500, Gregory Bush wrote:
> In the following example, is there a modifier I can use when
> declaring the notation so it doesn't hide the notation for sigT?
>
> Require Import List.
>
> (* So far so good *)
>
> Check {x : nat & {y | x < y}}.
>
> Notation "{ A , .. , B }" := (cons A .. (cons B nil) ..).
>
> (* Oops *)
>
> Check {x : nat & {y | x < y}}.
- [Coq-Club] Notation Question, Gregory Bush, 12/20/2012
- Re: [Coq-Club] Notation Question, Hugo Herbelin, 12/20/2012
- Re: [Coq-Club] Notation Question, Gregory Bush, 12/20/2012
- Re: [Coq-Club] Notation Question, Hugo Herbelin, 12/20/2012
- Re: [Coq-Club] Notation Question, Gregory Bush, 12/20/2012
- Re: [Coq-Club] Notation Question, Hugo Herbelin, 12/20/2012
Archive powered by MHonArc 2.6.18.