From 6451cad38d89760d644b08d9c5c62c5e0f64c6d8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Jan 2015 19:50:07 -0800
Subject: [PATCH] test(tests/lean/run): define list head using recursive
 equations

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

diff --git a/tests/lean/run/eq22.lean b/tests/lean/run/eq22.lean
new file mode 100644
index 000000000..fae15af6a
--- /dev/null
+++ b/tests/lean/run/eq22.lean
@@ -0,0 +1,9 @@
+import data.list
+open list
+
+definition head {A : Type} : Π (l : list A), l ≠ nil → A,
+head nil h      := absurd rfl h,
+head (a :: l) _ := a
+
+theorem head_cons {A : Type} (a : A) (l : list A) (h : a :: l ≠ nil) : head (a :: l) h = a :=
+rfl