test(tests/lean/run): add test/example

add test/example that defines count_vars using tactics and recursors.

see #662 for original definition, and e3a0e62859 for the fix that
allows us to use recursive equations.
The recursive equations are compiled into recursors.

tests/lean/run/662b.lean

@@ -0,0 +1,55 @@
+open nat
+
+inductive type : Type :=
+| Nat  : type
+| Func : type → type → type
+
+open type
+
+section var
+variable {var : type → Type}
+
+inductive term : type → Type :=
+| Var   : ∀ {t}, var t → term t
+| Const : nat → term Nat
+| Plus  : term Nat → term Nat → term Nat
+| Abs   : ∀ {dom ran}, (var dom → term ran) → term (Func dom ran)
+| App   : ∀ {dom ran}, term (Func dom ran) → term dom → term ran
+| Let   : ∀ {t1 t2}, term t1 → (var t1 → term t2) → term t2
+end var
+
+open term
+
+definition Term t := Π (var : type → Type), @term var t
+open unit
+
+-- Define count_vars using tactics
+definition count_vars1 {t : type} (T : @term (λ x, unit) t) : nat :=
+begin
+  induction T,
+    {exact 1},
+    {exact 0},
+    {exact v_0 + v_1},
+    {exact v_0 star},
+    {exact v_0 + v_1},
+    {exact v_0 + v_1 star},
+end
+
+-- Define count_vars using recursor
+definition count_vars2 {t : type} (T : @term (λ x, unit) t) : nat :=
+term.rec_on T
+  (λ t u, 1)
+  (λ n, 0)
+  (λ T₁ T₂ n₁ n₂, n₁ + n₂)
+  (λ d r f n, n star)
+  (λ d r T₁ T₂ n₁ n₂, n₁ + n₂)
+  (λ t₁ t₂ T₁ T₂ n₁ n₂, n₁ + n₂ star)
+
+definition var (t : type) : @term (λ x, unit) t :=
+Var star
+
+example : count_vars1 (App (App (var (Func Nat (Func Nat Nat))) (var Nat)) (var Nat)) = 3 :=
+rfl
+
+example : count_vars2 (App (App (var (Func Nat (Func Nat Nat))) (var Nat)) (var Nat)) = 3 :=
+rfl