fix(library/blast/recursor_action): indexed families

src/library/blast/hypothesis.h

@@ -72,6 +72,12 @@ public:
             m_buffer.push_back(h);
         }
     }
+
+    void erase(hypothesis_idx h) {
+        m_set.erase(h);
+        m_buffer.erase(h);
+    }
+
     unsigned size() const { return m_buffer.size(); }
     bool empty() const { return m_buffer.empty(); }
     hypothesis_idx_buffer const & as_buffer() const {

src/library/blast/recursor_action.cpp

@@ -194,6 +194,11 @@ action_result recursor_action(hypothesis_idx hidx, name const & R) {
     s.collect_direct_forward_deps(hidx, to_revert);
     for (auto i : indices)
         s.collect_direct_forward_deps(href_index(i), to_revert);
+    if (!indices.empty()) {
+        // If the set of indices is not empty, then we must remove hidx from to_revert,
+        // since it depends on the indices.
+        to_revert.erase(hidx);
+    }
     revert(to_revert);
 
     expr target       = s.get_target();

tests/lean/run/blast_recursor1.lean

@@ -0,0 +1,16 @@
+constants P Q : nat → Prop
+inductive foo : nat → Prop :=
+| intro1 : ∀ n, P n → foo n
+| intro2 : ∀ n, P n → foo n
+
+definition bar (n : nat) : foo n → P n :=
+by blast
+
+print bar
+/-
+definition bar : ∀ (n : ℕ), foo n → P n :=
+foo.rec (λ (n : ℕ) (H.3 : P n), H.3) (λ (n : ℕ) (H.3 : P n), H.3)
+-/
+
+definition baz (n : nat) : foo n → foo n ∧ P n :=
+by blast --loops