From 264cedb3a6040e0925fac855c1ccb61454cb1e68 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Feb 2015 20:02:49 -0800 Subject: [PATCH] fix(frontends/lean/rewrite_tactic): incorrect assertion --- src/library/tactic/rewrite_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index ebe537d21..9dcffde40 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -289,7 +289,7 @@ rewrite_info const & get_rewrite_info(expr const & e) { expr mk_rewrite_tactic_expr(buffer const & elems) { lean_assert(std::all_of(elems.begin(), elems.end(), [](expr const & e) { - return is_rewrite_step(e) || is_rewrite_unfold_step(e); + return is_rewrite_step(e) || is_rewrite_unfold_step(e) || is_rewrite_reduce_step(e); })); return mk_app(*g_rewrite_tac, mk_expr_list(elems.size(), elems.data())); }