From afa2f9b74c877adc29b219aaf370caaf852e88bc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Sep 2020 05:41:02 -0700
Subject: [PATCH] test: add old Lean3 tests

---
 tests/lean/run/def10.lean | 18 ++++++++++++++++
 tests/lean/run/def8.lean  | 43 +++++++++++++++++++++++++++++++++++++++
 tests/lean/run/def9.lean  | 22 ++++++++++++++++++++
 3 files changed, 83 insertions(+)
 create mode 100644 tests/lean/run/def10.lean
 create mode 100644 tests/lean/run/def8.lean
 create mode 100644 tests/lean/run/def9.lean

diff --git a/tests/lean/run/def10.lean b/tests/lean/run/def10.lean
new file mode 100644
index 0000000000..4cf71350c1
--- /dev/null
+++ b/tests/lean/run/def10.lean
@@ -0,0 +1,18 @@
+new_frontend
+
+def f : Bool → Bool → Nat
+| _, _ => 10
+
+example : f true true = 10 :=
+rfl
+
+def g : Bool → Bool → Bool → Nat
+| true, _,    true  => 1
+| _,   false, false => 2
+| _,   _,     _     => 3
+
+theorem ex1 : g true true true = 1 := rfl
+theorem ex2 : g true false true = 1 := rfl
+theorem ex3 : g true false false = 2 := rfl
+theorem ex4 : g false false false = 2 := rfl
+theorem ex5 : g false true true = 3 := rfl
diff --git a/tests/lean/run/def8.lean b/tests/lean/run/def8.lean
new file mode 100644
index 0000000000..eb5129b86b
--- /dev/null
+++ b/tests/lean/run/def8.lean
@@ -0,0 +1,43 @@
+new_frontend
+
+def g : List Nat → List Nat → Nat
+| [],         y::ys => y
+| [],         ys    => 0
+| x1::x2::xs, ys    => g xs ys
+| x::xs,      y::ys => g xs ys + y
+| x::xs,      []    => g xs []
+
+universes u v
+
+inductive Imf {α β} (f : α → β) : β → Type _
+| mk : (a : α) → Imf f (f a)
+
+def h {α β} {f : α → β} : {b : β} → Imf f b → α
+| _, Imf.mk a => a
+
+theorem ex1 {α β} (f : α → β) (a : α) : h (Imf.mk (f := f) a) = a :=
+rfl
+
+def v₁ : Imf Nat.succ 1 :=
+Imf.mk 0
+
+def v₂ : Imf (fun x => 1 + x) 1 :=
+Imf.mk 0
+
+theorem ex2 : h v₁ = 0 :=
+rfl
+
+theorem ex3 : h v₂ = 0 :=
+rfl
+
+theorem ex4 {α} : {a b : α} → a = b → b = a
+| _, _, rfl => rfl
+
+theorem ex5 {α} : {a b : α} → a = b → b = a
+| a, .(a), rfl => rfl
+
+theorem ex6 {α} : {a b : α} → a = b → b = a
+| a, .(a), Eq.refl .(a) => rfl
+
+theorem ex7 {α} : {a b : α} → a = b → b = a
+| .(a), a, Eq.refl .(a) => rfl
diff --git a/tests/lean/run/def9.lean b/tests/lean/run/def9.lean
new file mode 100644
index 0000000000..751a4ebceb
--- /dev/null
+++ b/tests/lean/run/def9.lean
@@ -0,0 +1,22 @@
+new_frontend
+
+def f : Nat → Nat → Nat
+| 100, 2 => 0
+| _,   4 => 1
+| _,   _ => 2
+
+theorem ex1 : f 100 2 = 0 := rfl
+theorem ex2 : f 9 4   = 1 := rfl
+theorem ex3 : f 8 4   = 1 := rfl
+theorem ex4 : f 6 3   = 2 := rfl
+
+inductive BV : Nat → Type
+| nil  : BV 0
+| cons : {n : Nat} → Bool → BV n → BV (n+1)
+
+open BV
+
+def g : {n : Nat} → BV n → Nat → Nat
+| _, cons b v, 1000000 => g v 0
+| _, cons b v, x       => g v (x + 1)
+| _, _,        _       => 1