max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/elaborator): non-recursive local shouldn't shadow projection

Browse source
This commit is contained in:
Sebastian Ullrich 2017-10-23 18:11:02 +02:00 • committed by Leonardo de Moura
parent 716c730c38
commit 032e0701e0
2 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/elaborator.cpp
View file

@ -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)) {

4
tests/lean/run/local_shadowing_projection.lean Normal file
View file

@ -0,0 +1,4 @@
namespace prod
def foo (a : nat × nat) (cmp : nat) :=
a.cmp
end prod