diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 1dbedf9a3..134c56724 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1113,6 +1113,7 @@ class pp_fn { } else if (is_let(e)) { if (is_prefix_of(prefix, let_name(e))) throw found_prefix(); } + return true; }; try { for_each_fn visitor(f); diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 1ac4529d6..9fcbb4ad6 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -44,6 +44,7 @@ struct environment::imp { if (obj) w = std::max(w, obj.get_weight()); } + return true; }; for_each_fn visitor(proc); visitor(e); diff --git a/src/kernel/for_each.h b/src/kernel/for_each.h index e33f7199b..c3231a4d1 100644 --- a/src/kernel/for_each.h +++ b/src/kernel/for_each.h @@ -22,8 +22,8 @@ template class for_each_fn { std::unique_ptr m_visited; F m_f; - static_assert(std::is_same::type, void>::value, - "for_each_fn: return type of m_f is not void"); + static_assert(std::is_same::type, bool>::value, + "for_each_fn: return type of m_f is not bool"); void apply(expr const & e, unsigned offset) { if (is_shared(e)) { @@ -35,7 +35,8 @@ class for_each_fn { m_visited->insert(p); } - m_f(e, offset); + if (!m_f(e, offset)) + return; switch (e.kind()) { case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 4ff96a25e..538342b72 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -262,8 +262,11 @@ bool has_assigned_metavar(expr const & e, substitution const & s) { return false; } else { auto proc = [&](expr const & n, unsigned) { + if (!has_metavar(n)) + return false; if (is_metavar(n) && s.is_assigned(n)) throw found_assigned(); + return true; }; for_each_fn visitor(proc); try { @@ -342,6 +345,7 @@ bool has_metavar(expr const & e, expr const & m, substitution const & s) { has_metavar(s.get_subst(m2), m, s)) throw found_metavar(); } + return true; }; try { for_each_fn proc(f); diff --git a/src/kernel/occurs.cpp b/src/kernel/occurs.cpp index fd6a2a8cd..44188b964 100644 --- a/src/kernel/occurs.cpp +++ b/src/kernel/occurs.cpp @@ -27,11 +27,12 @@ namespace occurs_ns { struct found {}; } bool occurs(name const & n, context const * c, unsigned sz, expr const * es) { - auto visitor = [&](expr const & e, unsigned) -> void { + auto visitor = [&](expr const & e, unsigned) -> bool { if (is_constant(e)) { if (const_name(e) == n) throw occurs_ns::found(); } + return true; }; try { for_each(visitor, c, sz, es); @@ -42,9 +43,10 @@ bool occurs(name const & n, context const * c, unsigned sz, expr const * es) { } bool occurs(expr const & n, context const * c, unsigned sz, expr const * es) { - auto visitor = [&](expr const & e, unsigned) -> void { + auto visitor = [&](expr const & e, unsigned) -> bool { if (e == n) throw occurs_ns::found(); + return true; }; try { for_each(visitor, c, sz, es);