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

chore(library/compiler/lcnf): use _x_<idx> instead of _x.<idx>

Browse source 
This is a temporary change while we debug the new compiler.
This commit is contained in:
Leonardo de Moura 2018-09-11 17:58:54 -07:00
parent 72e99ea3ee
commit 8ee10e202f
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/compiler/lcnf.cpp
View file

@ -46,7 +46,10 @@ public:
return e;
} else {
expr type = infer_type(e);
expr fvar = m_lctx.mk_local_decl(m_ngen, name(m_x, m_next_idx), type, e);
/* Remark: we use `m_x.append_after(m_next_idx)` instead of `name(m_x, m_next_idx)`
because the resulting name is confusing during debugging: it looks like a projection application.
We should replace it with `name(m_x, m_next_idx)` when the compiler code gets more stable. */
expr fvar = m_lctx.mk_local_decl(m_ngen, m_x.append_after(m_next_idx), type, e);
m_next_idx++;
m_fvars.push_back(fvar);
return fvar;