From 20f70035dd41e5606f2fbbb707a8b24f83abdb82 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 22 Feb 2016 10:44:22 -0800 Subject: [PATCH] fix(frontends/lean/util): fixes #1007 --- src/frontends/lean/util.cpp | 7 ++++++- tests/lean/run/1007.lean | 19 +++++++++++++++++++ 2 files changed, 25 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/1007.lean diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 6c4605b05..fe1b198bc 100644 --- a/src/frontends/lean/util.cpp +++ b/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> 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)) { diff --git a/tests/lean/run/1007.lean b/tests/lean/run/1007.lean new file mode 100644 index 000000000..2bf207bed --- /dev/null +++ b/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