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

feat(frontends/lean/elaborator): save type information for binders

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-10 15:39:38 -08:00
parent 2a37611d1f
commit d95645bd89
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2098,7 +2098,8 @@ expr elaborator::visit_lambda(expr const & e, optional<expr> 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);
}