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

fix(library/tactic/induction_tactic): apply substitution to hypothesis type (it may contain metavars)

Browse source 
closes #876
This commit is contained in:
Leonardo de Moura 2015-12-10 09:49:17 -08:00
parent a507ac8594
commit 8b3cbb8fdd
2 changed files with 9 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

@ -298,15 +298,16 @@ public:
expr normalize_H_type(expr const & H) { expr normalize_H_type(expr const & H) {
lean_assert(is_local(H)); lean_assert(is_local(H));
expr H_type = m_subst.instantiate_all(mlocal_type(H));
if (m_rec_name) { if (m_rec_name) {
recursor_info info = get_recursor_info(m_env, *m_rec_name); recursor_info info = get_recursor_info(m_env, *m_rec_name);
name tname = info.get_type_name(); name tname = info.get_type_name();
type_checker_ptr aux_tc = mk_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) { return n == tname; }); type_checker_ptr aux_tc = mk_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) { return n == tname; });
return aux_tc->whnf(mlocal_type(H)).first; return aux_tc->whnf(H_type).first;
} else { } else {
has_recursors_pred pred(m_env); has_recursors_pred pred(m_env);
type_checker_ptr aux_tc = mk_type_checker(m_env, m_ngen.mk_child(), pred); type_checker_ptr aux_tc = mk_type_checker(m_env, m_ngen.mk_child(), pred);
return aux_tc->whnf(mlocal_type(H)).first; return aux_tc->whnf(H_type).first;
} }
} }

6
tests/lean/run/876.hlean Normal file
View file

@ -0,0 +1,6 @@
example : Σ(X : Type₀), X → unit :=
begin
fapply sigma.mk,
{ exact unit},
{ intro x, induction x, exact unit.star }
end