From d95645bd89a9bc55ffe4596e1fa2b59c412ff25f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Nov 2016 15:39:38 -0800 Subject: [PATCH] feat(frontends/lean/elaborator): save type information for binders --- src/frontends/lean/elaborator.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index cbc9c5c562..a4e9e6f3d9 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2098,7 +2098,8 @@ expr elaborator::visit_lambda(expr const & e, optional const & expected_ty } expr ref_d = get_ref_for_child(binding_domain(it), it); new_d = ensure_type(new_d, ref_d); - expr l = push_local(locals, binding_name(it), new_d, binding_info(it), ref_d); + expr l = copy_tag(binding_domain(it), push_local(locals, binding_name(it), new_d, binding_info(it), ref_d)); + save_identifier_info(l); it = binding_body(it); if (has_expected) { lean_assert(is_pi(ex)); @@ -2127,7 +2128,8 @@ expr elaborator::visit_pi(expr const & e) { expr ref_d = get_ref_for_child(binding_domain(it), it); new_d = ensure_type(new_d, ref_d); expr ref = binding_domain(it); - push_local(locals, binding_name(it), new_d, binding_info(it), ref); + expr l = copy_tag(binding_domain(it), push_local(locals, binding_name(it), new_d, binding_info(it), ref)); + save_identifier_info(l); parent_it = it; it = binding_body(it); }