From 913d4526cdee0f0feec2004e81ebfdfa1a85e5a8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Sep 2015 16:42:55 -0700 Subject: [PATCH] feat(library/blast/expr): improve performance of abstract_lrefs --- src/library/blast/expr.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/library/blast/expr.cpp b/src/library/blast/expr.cpp index 00f1c0caba..de66ecf3e9 100644 --- a/src/library/blast/expr.cpp +++ b/src/library/blast/expr.cpp @@ -559,8 +559,12 @@ expr instantiate_value_univ_params(declaration const & d, levels const & ls) { } expr abstract_lrefs(expr const & e, unsigned n, expr const * subst) { + if (!has_lref(e)) + return e; lean_assert(std::all_of(subst, subst+n, [](expr const & e) { return closed(e) && is_lref(e); })); return blast::replace(e, [=](expr const & m, unsigned offset) -> optional { + if (!has_lref(m)) + return some_expr(m); // skip: m does not contain lref's if (is_lref(m)) { unsigned i = n; while (i > 0) {