michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(kernel/type_checker): bug in the app_delayed_justification object

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-25 10:09:45 -07:00
parent f981a4c1fe
commit 6ec5d768d0
1 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/kernel/type_checker.cpp
View file

@ -224,12 +224,18 @@ app_delayed_justification::app_delayed_justification(environment const & env, ex
justification app_delayed_justification::get() {
if (!m_jst) {
m_jst = mk_justification(app_arg(m_e),
// We should not have a reference to this object inside the closure.
// So, we create the following locals that will be captured by the closure instead of 'this'.
environment env = m_env;
expr e = m_e;
expr fn_type = m_fn_type;
expr arg_type = m_arg_type;
m_jst = mk_justification(app_arg(e),
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_app_type_mismatch(fmt, m_env, o,
subst.instantiate_metavars_wo_jst(m_e),
subst.instantiate_metavars_wo_jst(binding_domain(m_fn_type)),
subst.instantiate_metavars_wo_jst(m_arg_type));
return pp_app_type_mismatch(fmt, env, o,
subst.instantiate_metavars_wo_jst(e),
subst.instantiate_metavars_wo_jst(binding_domain(fn_type)),
subst.instantiate_metavars_wo_jst(arg_type));
});
}
return *m_jst;