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

fix(compiler/preprocess_rec): add extra comp_irrelevant step

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-04 17:17:45 -07:00
parent 37bc76ff09
commit 2e970d67ba
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/compiler/preprocess_rec.cpp
View file

@ -113,6 +113,7 @@ public:
v = eta_expand(m_env, v);
v = simp_pr1_rec(m_env, v);
v = inline_simple_definitions(m_env, v);
v = mark_comp_irrelevant_subterms(m_env, v);
v = lambda_lifting(m_env, v, m_aux_decls, d.is_trusted());
display(v);
// TODO(Leo)