The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I tried this:

  Notation "x -> y" := (forall x, y) (at level 99, right associativity, x binder, y at level 200).

and got

  Error: Type not allowed in recursive notation.

I tried

  Notation "x -> .. -> y -> P" := (forall x, .. (forall y, P) ..)

    (at level 200, x binder, y binder, right associativity) : type_scope.

based on

  Notation "∀  x .. y , P" := (forall x, .. (forall y, P) ..)

  (at level 200, x binder, y binder, right associativity) : type_scope.

in Coq.Init.Logic, and was told

  Error: A recursive notation must start with at least one symbol.

Note also that none of these notations have the potential to allow [A -> B] and [(x : A) -> B] to mean the same thing, because that is not how "binder" works.  Any further suggestions?  Should this go on the bug tracker as a feature request?

-Jason

On Sun, Dec 21, 2014 at 6:06 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 21/12/2014 23:25, Abhishek Anand wrote:
> Is there some way in Coq to write dependent
> function types in the former way?

Since at least coq trunk, the arrow is a notation defined in the prelude
as follows.

Reserved Notation "x -> y" (at level 99, right associativity, y at level
200).

I believe that using -noinit and tweaking this definition, you may
obtain what you're looking for.

PMP