From cda29ea107c7a049cddfabee47e05e3d3389dc2a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Jul 2016 09:32:12 -0400 Subject: [PATCH] fix(library/tactic/cases_tactic): incorrect mk_app --- src/library/tactic/cases_tactic.cpp | 2 +- tests/lean/run/cases_crash1.lean | 11 +++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/cases_crash1.lean diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 09b7c44b4c..0e31d69b17 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -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); diff --git a/tests/lean/run/cases_crash1.lean b/tests/lean/run/cases_crash1.lean new file mode 100644 index 0000000000..8b3475b39e --- /dev/null +++ b/tests/lean/run/cases_crash1.lean @@ -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