fix(frontends/lean/util): fixes #1007

src/frontends/lean/util.cpp

@@ -117,7 +117,12 @@ static void collect_locals_ignoring_tactics(expr const & e, collected_locals & l
 }
 
 void collect_annonymous_inst_implicit(parser const & p, collected_locals & ls) {
-    for (auto const & entry : p.get_local_entries()) {
+    buffer<pair<name, expr>> entries;
+    to_buffer(p.get_local_entries(), entries);
+    unsigned i = entries.size();
+    while (i > 0) {
+        --i;
+        auto const & entry = entries[i];
         if (is_local(entry.second) && !ls.contains(entry.second) && local_info(entry.second).is_inst_implicit() &&
             // remark: remove the following condition condition, if we want to auto inclusion also for non anonymous ones.
             p.is_anonymous_inst_name(entry.first)) {

tests/lean/run/1007.lean

@@ -0,0 +1,19 @@
+import algebra.group
+
+open algebra
+
+definition is_homomorphism [class] {G₁ G₂ : Type} [group G₁] [group G₂] (φ : G₁ → G₂) : Prop :=
+Π(g h : G₁), φ (g * h) = φ g * φ h
+
+-- set_option pp.all true
+
+definition apply_iso {G₁ G₂ : Type} [group G₁] [group G₂] {φ : G₁ → G₂} [H : is_homomorphism φ] (g h : G₁) : φ (g * h) = φ g * φ h :=
+H g h
+
+variables {G₁ G₂ : Type} (φ : G₁ → G₂) [group G₁] [group G₂] [is_homomorphism φ]
+
+theorem respect_one : φ 1 = 1 :=
+assert φ (1 * 1) = φ 1 * φ 1, from apply_iso 1 1,
+assert φ 1 * 1 = φ 1 * φ 1,   by rewrite one_mul at this; rewrite mul_one; exact this,
+assert 1 = φ 1,               from mul_left_cancel this,
+eq.symm this