diff options
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/Notations3.out | 21 | ||||
-rw-r--r-- | test-suite/output/Notations3.v | 20 |
2 files changed, 41 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index bd24f3f61..cf69874ca 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -140,3 +140,24 @@ alist = [0; 1; 2] : list nat ! '{{x, y}}, x + y = 0 : Prop +exists x : nat, + nat -> + exists y : nat, + nat -> + exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x + y = 0 /\ u + t = 0 + : Prop +exists x : nat, + nat -> + exists y : nat, + nat -> + exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0 + : Prop +exists_true '{{x, y}}, +(let u := 0 in exists_true '{{z, t}}, x + y = 0 /\ z + t = 0) + : Prop +exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R), +(forall x : A, R x x) + : Prop +exists_true (x : nat) (A : Type) (R : A -> A -> Prop) +(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z + : Prop diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 773241f90..3e07fbce9 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -258,3 +258,23 @@ End B. (* for isolated "forall" (was not working already in 8.6) *) Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder). Check ! '(x,y), x+y=0. + +(* Check that the terminator of a recursive pattern is interpreted in + the correct environment of bindings *) +Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun y => forall z:nat, z=0 /\ P)) ..)) (at level 200, x binder). +Check exists_mixed x y '(u,t), x+y=0/\u+t=0. +Check exists_mixed x y '(z,t), x+y=0/\z+t=0. + +(* Check that intermediary let-in are inserted inbetween instances of + the repeated pattern *) +Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder). +Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. + +(* Check that generalized binders are correctly interpreted *) + +Module G. +Generalizable Variables A R. +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. |