test(tests/lean/run): add basic pattern matching compilation test

tests/lean/run/eq2.lean

@@ -0,0 +1,5 @@
+definition symm {A : Type} : Π {a b : A}, a = b → b = a,
+symm rfl := rfl
+
+definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c,
+trans rfl rfl := rfl

tests/lean/run/eq3.lean

@@ -0,0 +1,8 @@
+import data.vector
+open nat vector
+
+definition swap {A : Type} : Π {n}, vector A (succ (succ n)) → vector A (succ (succ n)),
+swap (a :: b :: vs) := b :: a :: vs
+
+example (n : nat) (a b : num) (v : vector num n) : swap (a :: b :: v) = b :: a :: v :=
+rfl