test(tests/lean/extra): more tests for equation elaborator

tests/lean/extra/rec3.lean

@@ -0,0 +1,8 @@
+set_option pp.implicit true
+set_option pp.notation false
+
+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/extra/rec4.lean

@@ -0,0 +1,9 @@
+import data.vector
+open nat vector
+
+set_option pp.implicit true
+set_option pp.notation false
+
+definition diag {A : Type} : Π {n}, vector (vector A n) n → vector A n,
+diag nil               := nil,
+diag ((a :: va) :: vs) := a :: diag (map tail vs)

tests/lean/extra/rec5.lean

@@ -0,0 +1,26 @@
+import data.list
+open nat list
+
+set_option pp.implicit true
+set_option pp.notation false
+
+definition filter {A : Type} (p : A → Prop) [H : decidable_pred p] : list A → list A,
+filter nil      := nil,
+filter (h :: t) := if p h then h :: filter t else filter t
+
+open decidable
+
+definition decidable_eq_nat : Π (a b : nat), decidable (a = b),
+decidable_eq_nat 0 0         := inl rfl,
+decidable_eq_nat 0 (x+1)     := inr (ne.symm (succ_ne_zero x)),
+decidable_eq_nat (x+1) 0     := inr (succ_ne_zero x),
+decidable_eq_nat (x+1) (y+1) :=
+  decidable.cases_on (decidable_eq_nat x y)
+    (λ Hp, inl (congr_arg succ Hp))
+    (λ Hn, inr (λ H : x+1 = y+1, absurd (succ.inj H) Hn))
+
+/-
+match (decidable_eq_nat x y) with
+  (inl Hp) := inl (congr_arg succ Hp),
+  (inr Hn) := inr (λ Hs, absurd (succ.inj Hs) Hn)
+-/