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

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

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-20 20:28:02 -07:00
parent 2d22bb8ea2
commit 029f374a69
2 changed files with 13 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -195,8 +195,9 @@ class induction_tac {
expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_goal_hyps, new_type)), new_goal_hyps);
goal new_g(new_meta, new_type);
new_goals.push_back(new_g);
rec = mk_app(rec, Fun(minor_args, Fun(new_deps, new_meta)));
rec_type = m_tc.whnf(instantiate(binding_body(rec_type), new_meta), m_cs);
expr rec_arg = Fun(minor_args, Fun(new_deps, new_meta));
rec = mk_app(rec, rec_arg);
rec_type = m_tc.whnf(instantiate(binding_body(rec_type), rec_arg), m_cs);
curr_pos++;
}
}

10
tests/lean/hott/610.hlean Normal file
View file

@ -0,0 +1,10 @@
import hit.type_quotient
attribute type_quotient.elim [recursor 6]
definition my_elim_on {A : Type} {R : A → A → Type} {P : Type} (x : type_quotient R)
(Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P :=
begin
induction x,
exact Pc a,
exact Pp H
end