michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/rewrite_tactic): incorrect assertion

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-05 20:02:49 -08:00
parent e17ba27596
commit 264cedb3a6
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/rewrite_tactic.cpp
View file

@ -289,7 +289,7 @@ rewrite_info const & get_rewrite_info(expr const & e) {
expr mk_rewrite_tactic_expr(buffer<expr> const & elems) { expr mk_rewrite_tactic_expr(buffer<expr> const & elems) {
lean_assert(std::all_of(elems.begin(), elems.end(), [](expr const & e) { 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())); return mk_app(*g_rewrite_tac, mk_expr_list(elems.size(), elems.data()));
} }