test(tests/lean/run) define vector last and unzip functions using recursive equations

tests/lean/run/eq18.lean

@@ -0,0 +1,12 @@
+import data.vector
+open nat vector
+
+definition last {A : Type} : Π {n}, vector A (succ n) → A,
+last (a :: nil) := a,
+last (a :: v)   := last v
+
+theorem last_cons_nil {A : Type} {n : nat} (a : A) : last (a :: nil) = a :=
+rfl
+
+theorem last_cons {A : Type} {n : nat} (a : A) (v : vector A (succ n)) : last (a :: v) = last v :=
+rfl

tests/lean/run/eq19.lean

@@ -0,0 +1,15 @@
+import data.vector data.prod
+open nat vector prod
+
+variables {A B : Type}
+
+definition unzip : Π {n}, vector (A × B) n → vector A n × vector B n,
+unzip nil           := (nil, nil),
+unzip ((a, b) :: t) := (a :: pr₁ (unzip t), b :: pr₂ (unzip t))
+
+theorem unzip_nil : unzip nil = (@nil A, @nil B) :=
+rfl
+
+theorem unzip_cons {n : nat} (a : A) (b : B) (t : vector (A × B) n) :
+  unzip ((a, b) :: t) = (a :: pr₁ (unzip t), b :: pr₂ (unzip t)) :=
+rfl