test: new tests for structural recursion

@Kha The structural recursion is working :)
It is so much more powerful than the one in Lean3.
I added examples with `let rec`, nested and multiple
`match`-expressions.
I will keep testing and adding missing features tomorrow, and
will hopefully start porting stdlib to new frontend before the end of
the week.

tests/lean/run/structuralRec1.lean

@@ -18,3 +18,39 @@ rfl
 
 theorem ex5 {α β} (f : α → β) : map f [] = [] :=
 rfl
+
+def map2 {α β} (f : α → β) (as : List α) : List β :=
+let rec loop : List α → List β
+ | []    => []
+ | a::as => f a :: loop as;
+loop as
+
+theorem ex6 {α β} (f : α → β) (a : α) (as : List α) : map2 f (a::as) = (f a) :: map2 f as :=
+rfl
+
+def foo (xs : List Nat) : List Nat :=
+match xs with
+| []    => []
+| x::xs =>
+  let y := 2 * x;
+  match xs with
+  | []    => []
+  | x::xs => (y + x) :: foo xs
+
+#eval foo [1, 2, 3, 4]
+
+theorem fooEq (x y : Nat) (xs : List Nat) : foo (x::y::xs) = (2*x + y) :: foo xs :=
+rfl
+
+def bla (x : Nat) (ys : List Nat) : List Nat :=
+if x % 2 == 0 then
+  match ys with
+  | []    => []
+  | y::ys => (y + x/2) :: bla (x/2) ys
+else
+  match ys with
+  | []    => []
+  | y::ys => (y + x/2 + 1) :: bla (x/2) ys
+
+theorem blaEq (y : Nat) (ys : List Nat) : bla 4 (y::ys) = (y+2) :: bla 2 ys :=
+rfl