Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Notation Question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Notation Question


Chronological Thread 
  • 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}}.



Archive powered by MHonArc 2.6.18.

Top of Page