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

fix(library/equations_compiler/wf_rec): do not generate code for auxiliary *._pack functions added by equation compiler

Browse source 
In the new equation compiler, we should not generate code in the
equation compiler.
This commit is contained in:
Leonardo de Moura 2018-09-12 22:05:52 -07:00
parent 20f31c85bf
commit 23e5136ea2
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/equations_compiler/wf_rec.cpp
View file

@ -311,7 +311,9 @@ struct wf_rec_fn {
fn = mk_fix(fn);
expr fn_type = ctx.infer(fn);
expr r;
std::tie(m_env, r) = mk_aux_definition(m_env, get_options(), m_mctx, m_lctx, header,
equations_header new_header = header;
new_header.m_gen_code = false;
std::tie(m_env, r) = mk_aux_definition(m_env, get_options(), m_mctx, m_lctx, new_header,
head(header.m_fn_names), head(header.m_fn_actual_names),
fn_type, fn);
return r;