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

fix(frontends/lean/elaborator): make sure elaborated term is based on what the user wrote

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-27 18:49:48 -07:00
parent af7060b46e
commit 7b37762231
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -769,6 +769,8 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer<
pp_indent(pp_fn, infer_type(new_arg)) +
line() + format("but is expected to have type") +
pp_indent(pp_fn, new_arg_type));
} else {
new_args[i] = new_arg;
}
}
}
@ -851,6 +853,8 @@ optional<expr> elaborator::visit_app_propagate_expected(expr const & fn, buffer<
}
if (!is_def_eq(args_mvars[i], new_arg)) {
throw elaborator_exception(ref_arg, "invalid application, type mismatch when assigning auxiliary metavar");
} else {
new_args[size_at_args[i]] = new_arg;
}
}
return some_expr(mk_app(fn, new_args.size(), new_args.data()));