From 6b05146eca253460964c4dd177a0b86b48389206 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Apr 2014 17:29:47 -0700 Subject: [PATCH] fix(kernel/type_checker): preserve bound variable name when inferring type of a lambda expression Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index f91738229..11014b790 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" namespace lean { + /** \brief Auxiliary functional object used to implement type checker. */ struct type_checker::imp { environment m_env; @@ -682,7 +683,7 @@ struct type_checker::imp { ensure_sort(t, binder_domain(e)); } auto b = open_binder_body(e); - r = Pi(b.second, binder_domain(e), infer_type_core(b.first, infer_only)); + r = mk_pi(binder_name(e), binder_domain(e), abstract_p(infer_type_core(b.first, infer_only), b.second)); break; } case expr_kind::Pi: {