diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Notations3.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 4 |
2 files changed, 6 insertions, 0 deletions
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 #. |