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

feat(library/compiler/csimp): inline recursive functions marked with [inline_if_reduce]

Browse source
This commit is contained in:
Leonardo de Moura 2018-11-09 10:15:47 -08:00
parent 182812a278
commit 37df96e3e7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1266,7 +1266,7 @@ class csimp_fn {
is_constant(e))) { /* We only inline constants if they are marked with the `[inline]` or `[inline_if_reduce]` attrs */
return none_expr();
}
if (is_recursive(c)) return none_expr();
if (!inline_if_reduce_attr && is_recursive(c)) return none_expr();
expr new_fn = instantiate_value_lparams(*info, const_levels(fn));
if (inline_if_reduce_attr && !inline_attr) {
return beta_reduce_if_not_cases(new_fn, e, is_let_val);