From 5a6a4b45c1689efa2867389e5ade8e383fc352b5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 14 Aug 2015 14:39:23 -0700
Subject: [PATCH] fix(library/definitional/equations): fixes #796

---
 src/library/definitional/equations.cpp |  2 +-
 src/util/list_fn.h                     |  9 +++++++++
 tests/lean/run/796.lean                | 11 +++++++++++
 3 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/796.lean

diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp
index e19f0eed6..1e04d9008 100644
--- a/src/library/definitional/equations.cpp
+++ b/src/library/definitional/equations.cpp
@@ -1496,7 +1496,7 @@ class equation_compiler_fn {
                                     << "trying to pattern match inductive datatype parameter '" << p << "'");
                     } else {
                         list<expr> new_local_ctx = remove(e.m_local_context, p);
-                        list<expr> new_patterns  = ::lean::remove(e.m_patterns, p);
+                        list<expr> new_patterns  = remove_ith(e.m_patterns, i);
                         expr       new_rhs       = fix_rec_arg(new_fn, new_new_fn, i, e.m_rhs);
                         e = replace(eqn(new_local_ctx, new_patterns, new_rhs), p, param);
                     }
diff --git a/src/util/list_fn.h b/src/util/list_fn.h
index 3ed994c27..f513bcc30 100644
--- a/src/util/list_fn.h
+++ b/src/util/list_fn.h
@@ -303,5 +303,14 @@ T const & get_ith(list<T> const & l, unsigned idx) {
     return idx == 0 ? head(l) : get_ith(tail(l), idx - 1);
 }
 
+/** \brief Remove the i-th element of the list (starting a 0) */
+template<typename T>
+list<T> remove_ith(list<T> const & l, unsigned idx) {
+    if (is_nil(l))
+        return l;
+    else
+        return idx == 0 ? tail(l) : cons(head(l), remove_ith(tail(l), idx-1));
+}
+
 list<unsigned> mk_list_range(unsigned from, unsigned to);
 }
diff --git a/tests/lean/run/796.lean b/tests/lean/run/796.lean
new file mode 100644
index 000000000..59845e29a
--- /dev/null
+++ b/tests/lean/run/796.lean
@@ -0,0 +1,11 @@
+import data.nat
+
+inductive Diff ( n : nat ) : nat -> Type :=
+| Base : Diff n n
+| Step : Π (m : nat), Diff n (nat.succ m) -> Diff n m
+
+definition checkDiff : Π (n m : nat), Diff n m -> Prop
+| n _ (Diff.Base n) := true
+| n m (Diff.Step m s) := checkDiff n _ s
+
+print checkDiff