From 0926dee83b832719553517212cd7daddae334ea1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Nov 2019 08:59:26 -0800 Subject: [PATCH] chore: remove dead code --- src/library/equations_compiler/elim_match.cpp | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 1f3eeaca8c..fb847a5a8c 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -599,17 +599,6 @@ struct elim_match_fn { return some_inaccessible(P); } - /** Replace local `x` in `e` with `renaming.find(x)` */ - expr apply_renaming(expr const & e, name_map const & renaming) { - return replace(e, [&](expr const & e, unsigned) { - if (is_local(e)) { - if (auto new_e = renaming.find(local_name(e))) - return some_expr(*new_e); - } - return none_expr(); - }); - } - expr get_next_pattern_of(list const & eqns, unsigned eqn_idx) { for (equation const & eqn : eqns) { lean_assert(eqn.m_patterns);