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

fix(library/tactic/cases_tactic): incorrect mk_app

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-20 09:32:12 -04:00
parent a66a1df3b0
commit cda29ea107
2 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/cases_tactic.cpp
View file

@ -210,7 +210,7 @@ struct cases_tactic_fn {
expr aux_type = ctx.mk_pi(ts, ctx.mk_pi(h_new, ctx.mk_pi(eqs, g.get_type())));
expr aux_mvar = m_mctx.mk_metavar_decl(g.get_context(), aux_type);
/* assign mvar := aux_mvar indices h refls */
m_mctx.assign(mvar, mk_app(mk_app(mk_app(aux_mvar, I_args.size() - m_nindices, I_args.end() - m_nindices), h), refls));
m_mctx.assign(mvar, mk_app(mk_app(mk_app(aux_mvar, m_nindices, I_args.end() - m_nindices), h), refls));
/* introduce indices j' and h' */
auto r = intron(m_env, m_opts, m_mctx, aux_mvar, m_nindices + 1, new_indices_H);
lean_assert(r);

11
tests/lean/run/cases_crash1.lean Normal file
View file

@ -0,0 +1,11 @@
open tactic
axiom Sorry : ∀ A : Type, A
inductive Enum : Type := ea | eb | ec | ed
noncomputable definition Enum_dec_eq [instance] : decidable_eq Enum :=
by do a ← intro "a", cases a,
b ← intro "b", cases b,
right >> reflexivity,
try (left >> intro "H" >>= cases),
repeat $ intros >> mk_const "Sorry" >>= apply