feat(kernel): use cheap_beta_reduce at infer_lambda too

This commit is contained in:
Leonardo de Moura 2018-10-20 17:28:45 -07:00
parent 0b38547e97
commit db647139a2

View file

@ -105,6 +105,7 @@ expr type_checker::infer_lambda(expr const & _e, bool infer_only) {
e = binding_body(e);
}
expr r = infer_type_core(instantiate_rev(e, fvars.size(), fvars.data()), infer_only);
r = cheap_beta_reduce(r);
return m_lctx.mk_pi(fvars, r);
}