From 66ba3c8a0bc470a8d3fcdceac5b4ea81debbf9cf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 18 Jul 2014 23:47:53 +0100 Subject: [PATCH] fix(frontends/lean/elaborator): bug in the elaborator reported by Jeremy Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 1e069585a..755ff63ba 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -745,11 +745,13 @@ public: expr f_type = f_t.second; lean_assert(is_pi(f_type)); if (!expl) { - while (is_pi(f_type) && binding_info(f_type).is_strict_implicit()) { + while (binding_info(f_type).is_strict_implicit()) { tag g = f.get_tag(); expr imp_arg = mk_placeholder_meta(some_expr(binding_domain(f_type)), g); f = mk_app(f, imp_arg, g); - f_type = whnf(instantiate(binding_body(f_type), imp_arg)); + auto f_t = ensure_fun(f); + f = f_t.first; + f_type = f_t.second; } } expr d_type = binding_domain(f_type);