test: add tests for some Lean3 issues

tests/lean/run/lean3_zulip_issues_1.lean

@@ -0,0 +1,52 @@
+example : Prop := ∀ n, (n:Nat) + n = n.succ
+example : Prop := ∀ n, n.succ = (n:Nat) + n
+example : Prop := ∀ n, (n:Nat) + n.succ = n
+example : Prop := ∀ n, n.succ + (n:Nat) = n
+example : Prop := ∀ n, (n.succ:Nat) + n = n
+example : Prop := ∀ n, (n:Nat).succ + n = n
+
+def fib: Nat → Nat
+| 0 => 0
+| 1 => 1
+| n + 2 => fib n + fib (n + 1)
+
+theorem fib50Eq : fib 50 = 12586269025 :=
+  rfl
+
+inductive type : Type
+  | A : type
+  | B  : type
+
+inductive val : type → Type
+  | cA : val type.A
+  | cB : val type.B
+
+inductive wrap : Type
+  | val : ∀ {t : type}, (val t) → wrap
+
+def f : wrap → Nat
+  | wrap.val val.cA => 1
+  | _ => 1
+
+example (a : Nat) : True := by
+  have ∀ n, n ≥ 0 → a ≤ a from fun _ _ => Nat.leRefl ..
+  exact True.intro
+
+example (ᾰ : Nat) : True := by
+  have ∀ n, n ≥ 0 → ᾰ ≤ ᾰ from fun _ _ => Nat.leRefl ..
+  exact True.intro
+
+inductive Vec.{u} (α : Type u) : Nat → Type u
+  | nil  : Vec α 0
+  | cons : α → {n : Nat} → Vec α n → Vec α (n+1)
+
+constant Vars : Type
+
+structure Lang :=
+  (funcs : Nat → Type)
+  (consts : Type)
+
+inductive Term (L : Lang) : Type
+  | const_term : L.consts → Term L
+  | var_term   : Vars → Term L
+  | func_term  (n : Nat) (f : L.funcs n) (v : Vec (Term L) n) : Term L