max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/compiler/simp_app_args): use ll_infer_type

Browse source
This commit is contained in:
Leonardo de Moura 2018-11-09 13:18:28 -08:00
parent d3ad1cbfe1
commit 19bf71eb9c
1 changed files with 2 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/compiler/simp_app_args.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include "kernel/instantiate.h"
#include "library/compiler/util.h"
#include "library/compiler/ll_infer_type.h"
namespace lean {
/* Make sure every argument of applications and projections is a free variable (or neutral element). */
@ -75,11 +76,7 @@ class simp_app_args_fn {
m_fvars.push_back(fvar);
return fvar;
} else if (is_constant(e)) {
expr type;
if (optional<constant_info> info = env().find(const_name(e)))
type = mk_runtime_type(m_st, m_lctx, info->get_type());
else
type = mk_enf_object_type(); // TODO(Leo): improve
expr type = ll_infer_type(env(), e);
expr fvar = m_lctx.mk_local_decl(ngen(), next_name(), type, e);
m_fvars.push_back(fvar);
return fvar;