diff --git a/src/library/print.cpp b/src/library/print.cpp index 49bbff4e56..4b9241d4e3 100644 --- a/src/library/print.cpp +++ b/src/library/print.cpp @@ -19,7 +19,7 @@ bool is_used_name(expr const & t, name const & n) { bool found = false; for_each(t, [&](expr const & e, unsigned) { if (found) return false; // already found - if ((is_constant(e) && const_name(e) == n) // t has a constant named n + if ((is_constant(e) && const_name(e).get_root() == n) // t has a constant starting with n || (is_local(e) && (mlocal_name(e) == n || local_pp_name(e) == n))) { // t has a local constant named n found = true; return false; // found it diff --git a/tests/lean/pp_shadowed_const.lean b/tests/lean/pp_shadowed_const.lean index a61708f80b..2acd96fe6a 100644 --- a/tests/lean/pp_shadowed_const.lean +++ b/tests/lean/pp_shadowed_const.lean @@ -1 +1,4 @@ def f : Π (x : nat) (b : bool), bool = bool := λ bool, _ + +def g (heq : 1 == 1) := heq.symm +#print g diff --git a/tests/lean/pp_shadowed_const.lean.expected.out b/tests/lean/pp_shadowed_const.lean.expected.out index eb1bae50ce..75d6472427 100644 --- a/tests/lean/pp_shadowed_const.lean.expected.out +++ b/tests/lean/pp_shadowed_const.lean.expected.out @@ -2,3 +2,5 @@ pp_shadowed_const.lean:1:55: error: don't know how to synthesize placeholder context: bool : ℕ ⊢ _root_.bool → _root_.bool = _root_.bool +def g : 1 == 1 → 1 == 1 := +λ (heq_1 : 1 == 1), heq.symm heq_1