diff options
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] |