Leonardo de Moura f7b6645b60 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.		2018-05-29 16:40:13 -07:00
..
lean	fix(frontends/lean/elaborator): add missing synthesize	2018-05-29 16:40:13 -07:00