The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-sb.de>]

Hello 

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?

-- 
Regards
Christian