From 7fa5c3e5dae52519149348c34ff065b73276ff13 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 12 Jul 2015 11:33:40 -0400
Subject: [PATCH] feat(library/tactic/unfold_rec): take '[recursor]'
 annotations into account at unfold_rec

---
 src/library/tactic/unfold_rec.cpp        |  7 +++++--
 tests/lean/unfold_rec3.lean              | 15 +++++++++++++++
 tests/lean/unfold_rec3.lean.expected.out |  4 ++++
 3 files changed, 24 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/unfold_rec3.lean
 create mode 100644 tests/lean/unfold_rec3.lean.expected.out

diff --git a/src/library/tactic/unfold_rec.cpp b/src/library/tactic/unfold_rec.cpp
index 4c8089bb8..25b0734dc 100644
--- a/src/library/tactic/unfold_rec.cpp
+++ b/src/library/tactic/unfold_rec.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/replace_visitor.h"
 #include "library/constants.h"
+#include "library/user_recursors.h"
 #include "library/tactic/location.h"
 
 extern void pp_detail(lean::environment const & env, lean::expr const & e);
@@ -60,9 +61,11 @@ class unfold_rec_fn : public replace_visitor_aux {
         throw exception("ill-formed expression");
     }
 
-    static bool is_rec_building_part(name const & n) {
+    bool is_rec_building_part(name const & n) {
         if (n == get_prod_pr1_name() || n == get_prod_pr2_name())
             return true;
+        if (is_user_defined_recursor(m_env, n))
+            return true;
         if (n.is_atomic() || !n.is_string())
             return false;
         char const * str = n.get_string();
@@ -343,7 +346,7 @@ public:
         m_ngen(ngen),
         m_force_unfold(force_unfold),
         m_tc(mk_type_checker(m_env, m_ngen.mk_child(), [](name const &) { return false; })),
-        m_norm_decl_tc(mk_type_checker(m_env, m_ngen.mk_child(), [](name const & n) { return !is_rec_building_part(n); })),
+        m_norm_decl_tc(mk_type_checker(m_env, m_ngen.mk_child(), [&](name const & n) { return !is_rec_building_part(n); })),
         m_to_unfold(to_unfold),
         m_occs(occs),
         m_occ_idx(0)
diff --git a/tests/lean/unfold_rec3.lean b/tests/lean/unfold_rec3.lean
new file mode 100644
index 000000000..8ee62ebf2
--- /dev/null
+++ b/tests/lean/unfold_rec3.lean
@@ -0,0 +1,15 @@
+open nat
+
+definition nrec [recursor] := @nat.rec
+
+definition myadd x y :=
+nrec y (λ n r, succ r) x
+
+theorem myadd_zero : ∀ n, myadd n 0 = n :=
+begin
+  intro n, induction n with n ih,
+  reflexivity,
+  esimp [myadd],
+  state,
+  rewrite ih
+end
diff --git a/tests/lean/unfold_rec3.lean.expected.out b/tests/lean/unfold_rec3.lean.expected.out
new file mode 100644
index 000000000..891756620
--- /dev/null
+++ b/tests/lean/unfold_rec3.lean.expected.out
@@ -0,0 +1,4 @@
+unfold_rec3.lean:13:2: proof state
+n : ℕ,
+ih : myadd n 0 = n
+⊢ succ (myadd n 0) = succ n