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

fix(library/tactic/induction_tactic): fixes #892

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-10 10:52:57 -08:00
parent 4ef58f1ba5
commit 7b29ee1666
2 changed files with 21 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/tactic/induction_tactic.cpp
View file

@ -332,11 +332,16 @@ public:
// last one
return execute(g, H, H_type, r);
} else {
list<name> saved_ids = m_ids;
constraint_seq saved_cs = m_cs;
substitution saved_subst = m_subst;
try {
flet<list<name>> save_ids(m_ids, m_ids);
flet<constraint_seq> save_cs(m_cs, m_cs);
return execute(g, H, H_type, r);
} catch (exception &) {}
} catch (exception &) {
m_ids = saved_ids;
m_cs = saved_cs;
m_subst = saved_subst;
}
}
}
}

13
tests/lean/hott/892.hlean Normal file
View file

@ -0,0 +1,13 @@
open is_trunc unit
protected definition trunc.elim {n : trunc_index} {A : Type} {P : Type}
[Pt : is_trunc n P] (H : A → P) : trunc n A → P :=
trunc.rec H
attribute trunc.rec [recursor 6]
attribute trunc.elim [recursor 6]
example (x : trunc -1 unit) : unit :=
begin
induction x, exact star
end