From d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Aug 2017 20:05:03 +0200 Subject: Allows recursive patterns for binders to be associative on the left. This makes treatment of recursive binders closer to the one of recursive terms. It is unclear whether there are interesting notations liable to use this, but this shall make easier mixing recursive binders and recursive terms as in next commits. Example of (artificial) notation that this commit supports: Notation "! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder). --- test-suite/output/Notations3.out | 2 ++ test-suite/output/Notations3.v | 4 ++++ 2 files changed, 6 insertions(+) (limited to 'test-suite/output') diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index cf69874ca..e114ea894 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -161,3 +161,5 @@ exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R), exists_true (x : nat) (A : Type) (R : A -> A -> Prop) (_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z : Prop +{{{{True, nat -> True}}, nat -> True}} + : Prop * Prop * Prop diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 3e07fbce9..a7fed3561 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -278,3 +278,7 @@ Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x. Check exists_true `{Reflexive A R}, forall x, R x x. Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z. End G. + +(* Allows recursive patterns for binders to be associative on the left *) +Notation "!! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder). +Check !! a b : nat # True #. -- cgit v1.2.3