fix(library/definitional/equations): fixes #796

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);
                     }

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);
 }

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