From b976aa1e49579b7b50cfb140cbac8cb6f4c881a7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 17 Jul 2016 09:28:56 +0200
Subject: More examples of recursive notations, with emphasis in reference
 manual.

Further work would include:

- Identify binders up to alpha-conversion (see #4932 with a list of
  binders of length at least 2, or #4592 on printing notations such as
  ex2).

A cool example that one could also consider supporting:

- Notation "[[ a , .. , b | .. | a , .. , b ]]" :=
    (cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..).
---
 doc/refman/RefMan-syn.tex        | 19 ++++++++++++++++++-
 test-suite/output/Notations3.out |  7 +++++++
 test-suite/output/Notations3.v   |  4 ++++
 3 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index e91480ded3..92107b750b 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -589,6 +589,14 @@ Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c )  * u |]" :=
   (t at level 39).
 \end{coq_example*}
 
+Recursive patterns can occur several times on the right-hand side.
+Here is an example:
+
+\begin{coq_example*}
+Notation "[> a , .. , b <]" :=
+  (cons a .. (cons b nil) .., cons b .. (cons a nil) ..).
+\end{coq_example*}
+
 Notations with recursive patterns can be reserved like standard
 notations, they can also be declared within interpretation scopes (see
 section \ref{scopes}).
@@ -634,7 +642,16 @@ empty. Here is an example of recursive notation with closed binders:
 \begin{coq_example*}
 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).
+  (at level 200, x closed binder, y closed binder, right associativity).
+\end{coq_example*}
+
+A recursive pattern for binders can be used in position of a recursive
+pattern for terms. Here is an example:
+
+\begin{coq_example*}
+Notation ``'FUNAPP' x .. y , f'' :=
+  (fun x => .. (fun y => (.. (f x) ..) y ) ..)
+  (at level 200, x binder, y binder, right associativity).
 \end{coq_example*}
 
 \subsection{Summary}
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 8b3fa31618..64317a9f83 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -25,3 +25,10 @@ ETA x y : nat, Nat.add
      : nat -> nat -> nat
 fun x y : nat => Nat.add x y
      : forall (_ : nat) (_ : nat), nat
+ETA x y : nat, le_S
+     : forall x y : nat, x <= y -> x <= S y
+fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f
+     : (forall x : nat * (bool * unit), ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))}
+where
+?T : [x : nat * (bool * unit) |- Type] 
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index d791042043..655a01c2d2 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -32,3 +32,7 @@ Check ETA x y, Nat.add.
 Unset Printing Notations.
 Check ETA (x:nat) (y:nat), Nat.add.
 Set Printing Notations.
+Check ETA x y, le_S.
+
+Notation "'CURRY' x .. y , f" := (fun x => .. (fun y => f (x, .. (y,tt) ..)) ..) (at level 200, x binder, y binder).
+Check fun f => CURRY (x:nat) (y:bool), f.
-- 
cgit v1.2.3