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

fix(src/library/equations_compiler/elim_match): handle mixing of inaccessible terms and variables

Browse source
This commit is contained in:
Johannes Hölzl 2017-02-27 20:56:57 -05:00 • committed by Leonardo de Moura
parent 04991692bf
commit f44cbb896c
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/equations_compiler/elim_match.cpp
View file

@ -601,7 +601,7 @@ struct elim_match_fn {
for (equation const & eqn : P.m_equations) {
equation new_eqn = eqn;
new_eqn.m_patterns = tail(eqn.m_patterns);
if (is_var_transition) {
if (is_var_transition || is_local(head(eqn.m_patterns))) {
new_eqn.m_subst = add_subst(eqn.m_subst, head(eqn.m_patterns), head(P.m_var_stack));
}
new_eqns.push_back(new_eqn);

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

@ -0,0 +1,4 @@
example {α : Type} {p q : α → Prop} {x : α} (h : ∀ y, p y → q y) (hx : q x) :
∀ y, x = y ∨ p y → q y
| x (or.inr p) := h x p
| ._ (or.inl rfl) := hx