From fdef3e54070161be8af5f5b861defebe29b64ebc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Jan 2015 11:05:16 -0800
Subject: [PATCH] feat(library/definitional/equations): add support for
 reflexive datatypes in the definitional package

---
 src/library/definitional/equations.cpp |  7 +++--
 tests/lean/run/eq10.lean               | 42 ++++++++++++++++++++++++++
 2 files changed, 47 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/eq10.lean

diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp
index 1aadfac26..4acce8866 100644
--- a/src/library/definitional/equations.cpp
+++ b/src/library/definitional/equations.cpp
@@ -1101,8 +1101,11 @@ class equation_compiler_fn {
                 }
                 return none_expr();
             } else if (is_pi(d)) {
-                // TODO(Leo)
-                return none_expr();
+                if (is_app(a)) {
+                    return to_below(instantiate(binding_body(d), app_arg(a)), a, mk_app(b, app_arg(a)));
+                } else {
+                    return none_expr();
+                }
             } else {
                 return none_expr();
             }
diff --git a/tests/lean/run/eq10.lean b/tests/lean/run/eq10.lean
new file mode 100644
index 000000000..2bd4bf768
--- /dev/null
+++ b/tests/lean/run/eq10.lean
@@ -0,0 +1,42 @@
+inductive formula :=
+eqf  : nat → nat → formula,
+andf : formula → formula → formula,
+impf : formula → formula → formula,
+notf : formula → formula,
+orf  : formula → formula → formula,
+allf : (nat → formula) → formula
+
+namespace formula
+  definition implies (a b : Prop) : Prop := a → b
+
+  definition denote : formula → Prop,
+  denote (eqf n1 n2)  := n1 = n2,
+  denote (andf f1 f2) := denote f1 ∧ denote f2,
+  denote (impf f1 f2) := implies (denote f1) (denote f2),
+  denote (orf f1 f2)  := denote f1 ∨ denote f2,
+  denote (notf f)     := ¬ denote f,
+  denote (allf f)     := ∀ n : nat, denote (f n)
+
+  theorem denote_eqf (n1 n2 : nat) : denote (eqf n1 n2) = (n1 = n2) :=
+  rfl
+
+  theorem denote_andf (f1 f2 : formula) : denote (andf f1 f2) = (denote f1 ∧ denote f2) :=
+  rfl
+
+  theorem denote_impf (f1 f2 : formula) : denote (impf f1 f2) = (denote f1 → denote f2) :=
+  rfl
+
+  theorem denote_orf (f1 f2 : formula) : denote (orf f1 f2) = (denote f1 ∨ denote f2) :=
+  rfl
+
+  theorem denote_notf (f : formula) : denote (notf f) = ¬ denote f :=
+  rfl
+
+  theorem denote_allf (f : nat → formula) : denote (allf f) = (∀ n, denote (f n)) :=
+  rfl
+
+  example : denote (allf (λ n₁, allf (λ n₂, impf (eqf n₁ n₂) (eqf n₂ n₁)))) =
+            (∀ n₁ n₂ : nat, n₁ = n₂ → n₂ = n₁) :=
+  rfl
+
+end formula