max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/tactic/unfold_tactic): fix style

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-18 20:20:54 -04:00
parent ceba74f24e
commit ed73dafa48
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/unfold_tactic.cpp
View file

@ -335,7 +335,7 @@ class unfold_rec_fn : public replace_visitor_aux {
expr const new_head = get_app_fn(new_e);
// TODO(Leo): create an option for the following conditions?
if (is_constant(new_head) && inductive::is_elim_rule(m_env, const_name(new_head))) {
//head is a recursor... so the unfold is probably not generating a nice result...
// head is a recursor... so the unfold is probably not generating a nice result...
throw fold_failed();
}
return fold_rec_fn(m_ctx, fn, args, k, rec_name, indices_pos, main_pos, rec_arg_pos)(new_e);