michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/defeq_simplifier): no need to reverse args

Browse source
This commit is contained in:
Daniel Selsam 2016-02-13 14:21:08 -08:00 committed by Leonardo de Moura
parent d521063dfb
commit 859a3d35ea
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/defeq_simplifier.cpp
View file

@ -157,10 +157,10 @@ class defeq_simplify_fn {
}
expr defeq_simplify_app(expr const & e) {
buffer<expr> args;
expr f = defeq_simplify(get_app_args(e, args));
for (unsigned i = 0; i < args.size(); ++i) args[i] = defeq_simplify(args[i]);
return mk_app(f, args);
buffer<expr> rev_args;
expr f = defeq_simplify(get_app_rev_args(e, rev_args));
for (unsigned i = 0; i < rev_args.size(); ++i) rev_args[i] = defeq_simplify(rev_args[i]);
return mk_rev_app(f, rev_args);
}
/* Rewriting */