The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

I have some trouble using recursive notations in Coq 8.4 beta

The following snippet comes from the documentation and works perfectly well

Notation "’mylet’ f x .. y :=  t ’in’ u":=
   (let f := fun x => .. (fun y => t) .. in u)
   (x closed binder, y closed binder, at level 200, right associativity).

Now, the following works perfectly well:

Notation "'FUN' x => B" := (fun x => B) (at level 0).
Notation "’mylet’ f x .. y :=  t ’in’ u":=
(let f := FUN x => .. (FUN y => t) .. in u)
      (x closed binder, y closed binder, at level 200, right associativity).

But, if the definition of FUN is more complicated, I cannot define the
notation "mylet" anymore, and get the error message

Notation "'FUN' x => B" := (fun n R x => B n R).
Notation "’mylet’ f x .. y :=  t ’in’ u":=
(let f := FUN x => .. (FUN y => t) .. in u)
      (x closed binder, y closed binder, at level 200, right associativity).

Toplevel input, characters 70-88:
Error: Cannot find where the recursive pattern starts.

From this I infer that (rightfully), the notation FUN is unfolded in
the definition of mylet, and that it is indeed more complicated to
find where this recursive pattern starts. Looking at the
documentation, I would like to be able to define _exactly_ what are
the recursive pattern, and the terminating expression. But I cannot
find how to do it, nor to find encodings of my original problem such
that the notation is accepted... Any ideas?

With best regards,
Thomas