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

fix(library/tactic/cases_tactic): missing case

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-12 17:39:55 -07:00
parent d79fbee421
commit cf30d31024
2 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -324,7 +324,11 @@ struct cases_tactic_fn {
lean_cases_trace(mvar, tout() << "converted heq => eq\n";);
return unify_eqs(mvar2, num_eqs, updating, new_intros, subst);
} else if (is_eq(H_type, A, lhs, rhs)) {
if (is_local(rhs) || is_local(lhs)) {
if (ctx.is_def_eq(lhs, rhs)) {
lean_cases_trace(mvar, tout() << "skip\n";);
expr mvar2 = clear(m_mctx, *mvar1, H);
return unify_eqs(mvar2, num_eqs - 1, updating, new_intros, subst);
} else if (is_local(rhs) || is_local(lhs)) {
lean_cases_trace(mvar, tout() << "substitute\n";);
hsubstitution extra_subst;
bool symm = !is_local(lhs) && is_local(rhs);

4
tests/lean/run/cases_bug3.lean Normal file
View file

@ -0,0 +1,4 @@
set_option new_elaborator true
theorem ex {A : Type} : ∀ {a a' : A}, a == a' → a = a'
| a .a (heq.refl .a) := eq.refl a