diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 99bca100d..788340643 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -93,18 +93,6 @@ substitution substitution::assign(name const & m, level const & l) const { return assign(m, l, justification()); } -void substitution::for_each(std::function const & fn) const { - m_expr_subst.for_each([=](name const & n, std::pair const & a) { - fn(n, a.first, a.second); - }); -} - -void substitution::for_each(std::function const & fn) const { - m_level_subst.for_each([=](name const & n, std::pair const & a) { - fn(n, a.first, a.second); - }); -} - std::pair substitution::d_instantiate_metavars(level const & l, bool use_jst, bool updt) { if (!has_param(l)) return mk_pair(l, justification()); diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index dfabb356e..7bb8a961d 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -47,8 +47,15 @@ public: substitution assign(name const & m, level const & t, justification const & j) const; substitution assign(name const & m, level const & t) const; - void for_each(std::function const & fn) const; - void for_each(std::function const & fn) const; + template + void for_each_expr(F && fn) const { + for_each(m_expr_subst, [=](name const & n, std::pair const & a) { fn(n, a.first, a.second); }); + } + + template + void for_each_level(F && fn) const { + for_each(m_level_subst, [=](name const & n, std::pair const & a) { fn(n, a.first, a.second); }); + } bool is_assigned(expr const & m) const { lean_assert(is_metavar(m)); return is_expr_assigned(mlocal_name(m)); } opt_expr_jst get_assignment(expr const & m) const { lean_assert(is_metavar(m)); return get_expr_assignment(mlocal_name(m)); } diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index f82ea7a48..8a2415098 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -46,13 +46,14 @@ void display_assumptions(std::ostream & out, justification const & j) { } static std::ostream & operator<<(std::ostream & out, substitution const & s) { - bool first = true; - s.for_each([&](name const & n, expr const & v, justification const & j) { - if (first) first = false; else out << "\n"; - out << "?" << n << " <- " << v << " {"; - display_assumptions(out, j); - out << "}"; - }); + // bool first = true; + // s.for_each([&](name const & n, expr const & v, justification const & j) { + // if (first) first = false; else out << "\n"; + // out << "?" << n << " <- " << v << " {"; + // display_assumptions(out, j); + // out << "}"; + // }); + s.for_each_expr([](name const &, expr const &, justification const &) {}); return out; } diff --git a/src/util/rb_map.h b/src/util/rb_map.h index 5ecd56473..e097b294a 100644 --- a/src/util/rb_map.h +++ b/src/util/rb_map.h @@ -62,7 +62,7 @@ public: ref operator[](K const & k) { return ref(*this, k); } template - void for_each(F f) const { + void for_each(F && f) const { auto f_prime = [&](entry const & e) { f(e.first, e.second); }; return m_map.for_each(f_prime); } @@ -90,7 +90,7 @@ rb_map erase(rb_map const & m, K const & k) { return r; } template -void for_each(rb_map const & m, F f) { +void for_each(rb_map const & m, F && f) { return m.for_each(f); } void open_rb_map(lua_State * L);