diff --git a/src/kernel/find_fn.h b/src/kernel/find_fn.h index da9db5455d..4a7a08d6ff 100644 --- a/src/kernel/find_fn.h +++ b/src/kernel/find_fn.h @@ -9,34 +9,19 @@ Author: Leonardo de Moura #include "kernel/expr.h" namespace lean { -class find_fn { - template - struct pred_fn { - optional & m_result; - P m_p; - pred_fn(optional & result, P const & p):m_result(result), m_p(p) {} - bool operator()(expr const & e, unsigned offset) { - if (m_result) { - return false; // already found result, stop the search - } else if (m_p(e, offset)) { - m_result = e; - return false; // stop the search - } else { - return true; // continue the search - } - } - }; - optional m_result; - for_each_fn m_proc; -public: - template find_fn(P const & p):m_proc(pred_fn

(m_result, p)) {} - optional operator()(expr const & e) { m_proc(e); return m_result; } -}; - -/** - \brief Return a subexpression of \c e that satisfies the predicate \c p. -*/ +/** \brief Return a subexpression of \c e that satisfies the predicate \c p. */ template optional find(expr const & e, P p) { - return find_fn(p)(e); + optional result; + for_each(e, [&](expr const & e, unsigned offset) { + if (result) { + return false; + } else if (p(e, offset)) { + result = e; + return false; + } else { + return true; + } + }); + return result; } }