diff options
Diffstat (limited to 'test-suite/output/Notations2.out')
| -rw-r--r-- | test-suite/output/Notations2.out | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 1ec701ae8..121a369a9 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -37,11 +37,22 @@ let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 λ (f : nat -> nat) (x : nat), f(x) + S(x) : (nat -> nat) -> nat -> nat Notation plus2 n := (S(S(n))) +λ n : list(nat), match n with + | 1 :: nil => 0 + | _ => 2 + end + : list(nat) -> nat +λ n : list(nat), +match n with +| 1 :: nil => 0 +| nil | 0 :: _ | 1 :: _ :: _ | plus2 _ :: _ => 2 +end + : list(nat) -> nat λ n : list(nat), match n with | nil => 2 | 0 :: _ => 2 -| list1 => 0 +| 1 :: nil => 0 | 1 :: _ :: _ => 2 | plus2 _ :: _ => 2 end @@ -84,3 +95,9 @@ a≡ : Set .α : Set +# a : .α => +# b : .α => +let res := 0 in +for i from 0 to a updating (res) +{{for j from 0 to b updating (res) {{S res}};; res}};; res + : .α -> .α -> .α |