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

fix(library/blast/intros): corner case

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-13 15:25:55 -08:00
parent 6c038626f8
commit 33036befc6
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/intros.cpp
View file

@ -24,6 +24,8 @@ struct intros_proof_step_cell : public proof_step_cell {
}; };
bool intros_action(unsigned max) { bool intros_action(unsigned max) {
if (max == 0)
return true;
state & s = curr_state(); state & s = curr_state();
expr target = whnf(s.get_target()); expr target = whnf(s.get_target());
if (!is_pi(target)) if (!is_pi(target))