From b6b520302d257bc49732d8a75a046dde2cf027a0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Dec 2013 15:35:26 -0800 Subject: [PATCH] feat(kernel/replace_visitor): relax replace_visitor contract, the input expression can be null Signed-off-by: Leonardo de Moura --- src/kernel/replace_visitor.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/kernel/replace_visitor.cpp b/src/kernel/replace_visitor.cpp index 12b867009a..c6c614ce93 100644 --- a/src/kernel/replace_visitor.cpp +++ b/src/kernel/replace_visitor.cpp @@ -52,7 +52,7 @@ expr replace_visitor::visit_pi(expr const & e, context const & ctx) { expr replace_visitor::visit_let(expr const & e, context const & ctx) { lean_assert(is_let(e)); return update_let(e, [&](expr const & t, expr const & v, expr const & b) { - expr new_t = t ? visit(t, ctx) : expr(); + expr new_t = visit(t, ctx); expr new_v = visit(v, ctx); expr new_b; { @@ -64,6 +64,8 @@ expr replace_visitor::visit_let(expr const & e, context const & ctx) { } expr replace_visitor::visit(expr const & e, context const & ctx) { check_system("expression replacer"); + if (!e) + return e; bool shared = false; if (is_shared(e)) { shared = true;