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

fix(library/compiler/csimp): missing simplification

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-14 09:36:13 -07:00
parent 2638a77a79
commit dc1b3aceda
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -133,7 +133,7 @@ class csimp_fn {
for (unsigned i = first_minor_idx; i < args.size(); i++) {
lean_assert(!empty(cnstrs));
if (head(cnstrs) == const_name(k)) {
return visit(beta_reduce(args[i], k_args.size() - nparams, k_args.data() + nparams));
return beta_reduce(args[i], k_args.size() - nparams, k_args.data() + nparams);
}
cnstrs = tail(cnstrs);
}
@ -171,7 +171,7 @@ class csimp_fn {
} else {
if (!is_atom(r))
r = mk_let_decl(r);
return mk_app(r, nargs - i, args + i);
return visit(mk_app(r, nargs - i, args + i));
}
}