From db647139a287d79f8edb452b48609652b348ad4f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 20 Oct 2018 17:28:45 -0700
Subject: [PATCH] feat(kernel): use `cheap_beta_reduce` at `infer_lambda` too

---
 src/kernel/type_checker.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 6889d79f58..5d50552965 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -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);
 }