michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(kernel/type_checker): preserve bound variable name when inferring type of a lambda expression

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-25 17:29:47 -07:00
parent 63b6564b78
commit 6b05146eca
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/type_checker.cpp
View file

@ -19,6 +19,7 @@ Author: Leonardo de Moura
#include "kernel/abstract.h" #include "kernel/abstract.h"
namespace lean { namespace lean {
/** \brief Auxiliary functional object used to implement type checker. */ /** \brief Auxiliary functional object used to implement type checker. */
struct type_checker::imp { struct type_checker::imp {
environment m_env; environment m_env;
@ -682,7 +683,7 @@ struct type_checker::imp {
ensure_sort(t, binder_domain(e)); ensure_sort(t, binder_domain(e));
} }
auto b = open_binder_body(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; break;
} }
case expr_kind::Pi: { case expr_kind::Pi: {