From 032e0701e0a15afd16c6b1087cd5d725fdf5f9bb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 23 Oct 2017 18:11:02 +0200 Subject: [PATCH] fix(frontends/lean/elaborator): non-recursive local shouldn't shadow projection --- src/frontends/lean/elaborator.cpp | 7 +++++-- tests/lean/run/local_shadowing_projection.lean | 4 ++++ 2 files changed, 9 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/local_shadowing_projection.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 1e7d03b11c..0d98c6d0fc 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2773,8 +2773,11 @@ elaborator::field_resolution elaborator::field_to_decl(expr const & e, expr cons if (auto p = find_field(m_env, const_name(I), fname)) return field_resolution(const_name(I), *p, fname); name full_fname = const_name(I) + fname; - if (auto ldecl = m_ctx.lctx().find_local_decl_from_user_name(full_fname.replace_prefix(get_namespace(env()), {}))) { - // recursive call + name local_name = full_fname.replace_prefix(get_namespace(env()), {}); + if (auto ldecl = m_ctx.lctx().find_if([&](local_decl const & ldecl) { + return ldecl.get_info().is_rec() && ldecl.get_pp_name() == local_name; + })) { + // projection is recursive call return field_resolution(full_fname, ldecl); } if (!m_env.find(full_fname)) { diff --git a/tests/lean/run/local_shadowing_projection.lean b/tests/lean/run/local_shadowing_projection.lean new file mode 100644 index 0000000000..595a0095b7 --- /dev/null +++ b/tests/lean/run/local_shadowing_projection.lean @@ -0,0 +1,4 @@ +namespace prod + def foo (a : nat × nat) (cmp : nat) := + a.cmp +end prod