From 4904f7657fccad90a69b69e648d01963f1bff66e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 9 Mar 2015 08:42:21 -0700
Subject: [PATCH] test(tests/lean/run): add definition package tests

---
 tests/lean/run/interp.lean | 30 ++++++++++++++++++++++++++++++
 tests/lean/run/parity.lean | 32 ++++++++++++++++++++++++++++++++
 2 files changed, 62 insertions(+)
 create mode 100644 tests/lean/run/interp.lean
 create mode 100644 tests/lean/run/parity.lean

diff --git a/tests/lean/run/interp.lean b/tests/lean/run/interp.lean
new file mode 100644
index 000000000..a5ddb61ed
--- /dev/null
+++ b/tests/lean/run/interp.lean
@@ -0,0 +1,30 @@
+import algebra.function
+open bool nat
+open function
+
+inductive univ :=
+| ubool  : univ
+| unat   : univ
+| uarrow : univ → univ → univ
+
+open univ
+
+definition interp : univ → Type₁
+| ubool          := bool
+| unat           := nat
+| (uarrow fr to) := interp fr → interp to
+
+definition foo : Π (u : univ) (el : interp u), interp u
+| ubool          tt := ff
+| ubool          ff := tt
+| unat           n  := succ n
+| (uarrow fr to) f  := λ x : interp fr, f (foo fr x)
+
+definition is_even : nat → bool
+| zero     := tt
+| (succ n) := bnot (is_even n)
+
+example : foo unat 10  = 11 := rfl
+example : foo ubool tt = ff := rfl
+example : foo (uarrow unat ubool) (λ x : nat, is_even x) 3 = tt := rfl
+example : foo (uarrow unat ubool) (λ x : nat, is_even x) 4 = ff := rfl
diff --git a/tests/lean/run/parity.lean b/tests/lean/run/parity.lean
new file mode 100644
index 000000000..fb4bd43b5
--- /dev/null
+++ b/tests/lean/run/parity.lean
@@ -0,0 +1,32 @@
+import data.nat
+open nat
+
+inductive Parity : nat → Type :=
+| even : ∀ n : nat, Parity (2 * n)
+| odd  : ∀ n : nat, Parity (2 * n + 1)
+
+open Parity
+
+definition parity : Π (n : nat), Parity n
+| parity 0     := even 0
+| parity (n+1) :=
+  begin
+    have aux : Parity n, from parity n,
+    cases aux with (k, k),
+    begin
+      apply (odd k)
+    end,
+    begin
+      change (Parity (2*k + 2*1)),
+      rewrite -mul.left_distrib,
+      apply (even (k+1))
+    end
+  end
+
+print definition parity
+
+definition half (n : nat) : nat :=
+match ⟨n, parity n⟩ with
+| ⟨⌞2 * k⌟,     even k⟩ := k
+| ⟨⌞2 * k + 1⌟, odd k⟩  := k
+end