aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Notations2.out
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/Notations2.out')
-rw-r--r--test-suite/output/Notations2.out6
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 6ffe56e11..41d159375 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -37,13 +37,13 @@ let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
: (nat -> nat) -> nat -> nat
Notation plus2 n := (S(S(n)))
λ n : list(nat), match n with
- | 1 :: nil => 0
+ | list1 => 0
| _ => 2
end
: list(nat) -> nat
λ n : list(nat),
match n with
-| 1 :: nil => 0
+| list1 => 0
| nil | 0 :: _ | 1 :: _ :: _ | plus2 _ :: _ => 2
end
: list(nat) -> nat
@@ -51,7 +51,7 @@ end
match n with
| nil => 2
| 0 :: _ => 2
-| 1 :: nil => 0
+| list1 => 0
| 1 :: _ :: _ => 2
| plus2 _ :: _ => 2
end