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

perf(library/tactic/simplifier/simplifier): minimize number of check_system invocations

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-08 21:53:33 -07:00
parent ec4cd87172
commit c49f51dccc
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/tactic/simplifier/simplifier.cpp
View file

@ -305,7 +305,6 @@ expr simplifier::whnf_eta(expr const & e) {
/* Simplification */
simp_result simplifier::simplify(expr const & e) {
check_system("simplifier");
m_num_steps++;
lean_trace_inc_depth("simplifier");
lean_trace_d("simplifier", tout() << m_rel << ": " << e << "\n";);
@ -350,6 +349,7 @@ simp_result simplifier::simplify(expr const & e) {
r = join(r, simplify_pi(r.get_new()));
break;
case expr_kind::App:
check_system("simplifier");
r = join(r, simplify_app(r.get_new()));
break;
case expr_kind::Let: