From f7279ee4199b18e9fdb5e1659a821d240d5279dc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Nov 2020 09:48:36 -0800
Subject: [PATCH] test: add tests for some Lean3 issues

---
 tests/lean/run/lean3_zulip_issues_1.lean | 52 ++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 tests/lean/run/lean3_zulip_issues_1.lean

diff --git a/tests/lean/run/lean3_zulip_issues_1.lean b/tests/lean/run/lean3_zulip_issues_1.lean
new file mode 100644
index 0000000000..ec273095ce
--- /dev/null
+++ b/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