fix(library/replace_visitor): remove replace_visitor_closed, it does not handle nested let-expr correctly

src/library/replace_visitor.cpp

@@ -77,13 +77,4 @@ expr replace_visitor::visit(expr const & e) {
 
     lean_unreachable(); // LCOV_EXCL_LINE
 }
-
-expr replace_visitor_closed::visit_binding(expr const & e) {
-    // TODO(Leo): improve performance by grouping calls to abstract_locals and instantiate.
-    lean_assert(is_binding(e));
-    expr new_d = visit(binding_domain(e));
-    expr new_l = mk_local(mk_fresh_name(), binding_name(e), new_d, binding_info(e));
-    expr new_b = visit(instantiate(binding_body(e), new_l));
-    return update_binding(e, new_d, abstract_local(new_b, new_l));
-}
 }

src/library/replace_visitor.h

@@ -35,12 +35,4 @@ public:
     expr operator()(expr const & e) { return visit(e); }
     void clear() { m_cache.clear(); }
 };
-
-/** \brief A replace_visitor class that provides a default visit_binding implementation
-    that replaces de-Bruijn variables with local constants.
-    Thus, any visited term is guaranteed to be closed. */
-class replace_visitor_closed : public replace_visitor {
-protected:
-    virtual expr visit_binding(expr const &) override;
-};
 }