test: add old Lean3 tests

tests/lean/run/def2.lean

@@ -0,0 +1,21 @@
+new_frontend
+
+inductive Vec.{u} (α : Type u) : Nat → Type u
+| nil  : Vec α 0
+| cons : α → {n : Nat} → Vec α n → Vec α (n+1)
+
+open Vec
+universes u
+
+variables {α : Type u}
+variables (f : α → α → α)
+
+def mapHead1 : {n : Nat} → Vec α n → Vec α n → Vec α n
+| _, nil, nil => nil
+| _, cons a va, cons b bv => cons (f a b) va
+
+theorem ex1 : mapHead1 f nil nil = nil :=
+rfl
+
+theorem ex2 (a b : α) (n : Nat) (va vb : Vec α n) : mapHead1 f (cons a va) (cons b vb) = cons (f a b) va :=
+rfl

tests/lean/run/def3.lean

@@ -0,0 +1,10 @@
+new_frontend
+
+abbrev N := Nat
+
+def f : N → Nat
+| 0   => 1
+| n+1 => n
+
+theorem ex1 : f 0 = 1 :=
+rfl