The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi all,

Is there a way of getting a non-recursive notation to understand
binders like in recursive notations? For instance, with recursive
notations I can do the following silly notation:

Notation "'rec' x1 .. xn '|' f" := ((fun x1 => .. (fun xn => f) .. ))
  (at level 60, x1 binder, xn binder).

and then write examples with optional type annotations:

Definition idnat := rec x : nat | x.

Definition id := rec A (x : A) | x.


But I don't find a way of getting the same result with a fixed number
of binders. I.e,

Notation "'notrec' x y '|' f" := (fun x => (fun y => f))
  (at level 60, x binder, y binder).

throws error

Error: Type not allowed in recursive notation.

and

Notation "'notrec' x y '|' f" := (fun x => (fun y => f))
  (at level 60, x at next level, y at next level).

doesn't understand the type notation, i.e.,

Definition id := notrec A (x : A) | x.

throws error

Toplevel input, characters 34-35:
Syntax error: [constr:operconstr] expected after [constr:operconstr]
(in [constr:operconstr]).


In my particular development I have 3 binders in my notation, and I'd
like not to make an exponentially amount of notations to account for
the optional typing of each of them.


Thanks in advance,
Beta