From f7b6645b606fd5ce575e56478c60d562f1d70944 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 May 2018 16:40:13 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): add missing `synthesize` We added for the following reasons: 1- It should mimic the behavior of `visit_lambda` and `visit_pi`. 2- It minimizes the number of auxiliary metavariables that need to be created when we execute `locals.mk_lambda(new_body)`. In Lean3, it would minimize the number of delayed abstractions. --- src/frontends/lean/elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7b47567966..70a2e0bb75 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -3523,7 +3523,7 @@ expr elaborator::visit_let(expr const & e, optional const & expected_type) save_identifier_info(l); expr body = instantiate_rev_locals(let_body(e), locals); expr new_body = visit(body, expected_type); - /* TODO(Leo): add synthesize here? */ + synthesize(); expr new_e = locals.mk_lambda(new_body); return new_e; }