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

feat(library/compiler/csimp): avoid unnecessary let-decls

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-14 16:21:37 -07:00
parent 8840f340aa
commit 768a45b7f9
1 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/compiler/csimp.cpp
View file

@ -60,10 +60,14 @@ class csimp_fn {
}
expr mk_let_decl(expr const & e) {
expr type = infer_type(e);
expr fvar = m_lctx.mk_local_decl(ngen(), next_name(), type, e);
m_fvars.push_back(fvar);
return fvar;
if (is_atom(e)) {
return e;
} else {
expr type = infer_type(e);
expr fvar = m_lctx.mk_local_decl(ngen(), next_name(), type, e);
m_fvars.push_back(fvar);
return fvar;
}
}
expr visit_let(expr e) {