diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-12 13:42:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:03 +0100 |
| commit | 65505b835d6a77b8702d11d09e8cf6b84c529c65 (patch) | |
| tree | 68a124a0211c520f4e87bb0fc6bf2166b125676b /test-suite | |
| parent | 09122b77b4f556281fec338cbb2ec43c5520dc8d (diff) | |
Adding support for re-folding notation referring to isolated "forall '(x,y), t".
Was apparently forgotten in a67bd7f9.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations3.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 5 |
2 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 1b5725275..bd24f3f61 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -138,3 +138,5 @@ amatch = mmatch 0 (with 0 => 1| 1 => 2 end) : unit alist = [0; 1; 2] : list nat +! '{{x, y}}, x + y = 0 + : Prop diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index a8d6c97fb..773241f90 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -253,3 +253,8 @@ Definition alist := [0;1;2]. Print alist. End B. + +(* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *) +(* 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. |