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

fix(library/tactic/rewrite_tactic): assertion violation when checking

Browse source 
dependencies at rewrite tactic
This commit is contained in:
Leonardo de Moura 2015-04-30 15:41:57 -07:00
parent 936e024128
commit d546b019fb
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -405,7 +405,8 @@ optional<goal> move_after(name_generator & ngen, goal const & g, name const & h,
for (unsigned i = 0; i < hyps.size(); i++) {
expr const & h_2 = hyps[i];
if (std::any_of(hs.begin(), hs.end(), [&](name const & n) { return mlocal_name(h_2) == n; })) {
if (depends_on(to_move.size(), to_move.begin(), mlocal_type(h_2)))
if (std::any_of(to_move.begin(), to_move.end(),
[&](expr const & h) { return depends_on(mlocal_type(h_2), h); }))
return optional<goal>(); // can't move
num_found++;
new_hyps.push_back(h_2);
@ -424,7 +425,8 @@ optional<goal> move_after(name_generator & ngen, goal const & g, name const & h,
} else if (mlocal_name(h_2) == h) {
lean_assert(to_move.empty());
to_move.push_back(h_2);
} else if (depends_on(to_move.size(), to_move.begin(), mlocal_type(h_2))) {
} else if (std::any_of(to_move.begin(), to_move.end(),
[&](expr const & h) { return depends_on(mlocal_type(h_2), h); })) {
to_move.push_back(h_2);
} else {
new_hyps.push_back(h_2);