diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-29 18:30:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-29 18:45:46 +0200 |
| commit | 8ad6bf357284f3fcfd94f08561450bb5bf38ad36 (patch) | |
| tree | 0875a95610c22592eaf52a15bb0d9dd502aad914 /test-suite/output/Notations3.out | |
| parent | e128900aee63c972d7977fd47e3fd21649b63409 (diff) | |
Fixes #7110 ("as" untested while looking for notation for nested patterns).
Diffstat (limited to 'test-suite/output/Notations3.out')
| -rw-r--r-- | test-suite/output/Notations3.out | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 1987b6a6e..304353f55 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -223,3 +223,11 @@ fun S : nat => [[S | S.S]] : Set exists2 '{{y, z}} : nat * nat, y > z & z > y : Prop +foo = +fun l : list nat => match l with + | _ :: (_ :: _) as l1 => l1 + | _ => l + end + : list nat -> list nat + +Argument scope is [list_scope] |