The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> Im Experimenting with Notations (for Ensembles)
> 
> Require Export Ensembles Finite_sets.
> 
> Implicit Arguments In [U].
> Implicit Arguments Finite [U].
> Implicit Arguments Included [U].
> Implicit Arguments Add [U].
> 
> Notation "{{ x , .. , y }}" := ( Add .. (Add (Empty_set _) x) .. y) (at 
> level 0, x at level 99).
> 
> Notation "{{ x : A | P }}" := (fun x : A => (P : Prop ))(at level 0, x at 
> level 99).
> Notation "{{ x | P }}" := (fun x => (P : Prop ))(at level 0, x at level 99).
> 
> Goal forall x y z , Included {{ x , y }} {{ x , y , z }}.
> 
> (* 
>    Toplevel input, characters 112-113:
>    Syntax error: '|' or ':' expected after [constr:operconstr level 99] (in 
> [constr:operconstr]).
> *)
> 
> I understand that due to the LL1 nature of the Notation Parser the
> common initial parts of all the notations need to be at the same level. 
> 
> Each of the two notation groups in isolation works as expected but is
> there a way to keep the second group from hiding the recursive notation?

As shown by "Print Grammar constr", the "{{ x , .. , y }}" is in fact
not factorized with the other "{{ }}" notations.

  ...
  [ "{{"; constr:operconstr LEVEL "99"; "|"; constr:operconstr LEVEL "200";
    "}}"
  | "{{"; constr:operconstr LEVEL "99"; ":"; constr:operconstr LEVEL "200";
    "|"; constr:operconstr LEVEL "200"; "}}"
  | "{{"; LIST1 (constr:operconstr LEVEL "99") SEP [ "," ]; "}}"
  ...

You can solve the problem by splitting your recursive notations in two
parts as follows:

Notation "{{ x }}" := (Add (Empty_set _) x) (at level 0, x at level 99).
Notation "{{ z , x , .. , y }}" := ( Add .. (Add (Add (Empty_set _) z) x) .. 
y) (at level 0, z at level 99).

This by the way suggests that Coq applies this decomposition
automatically. We'll try.

Hugo Herbelin