030f53fa43
The unifier used to implement the `cases` tactic should not discard equations of the form `x = t` and `t = x` using proof irrelanvance. The new test demonstrates the issue. The unifier was reaching the state ``` x : Conw Con.nil |- x = Conw.nilw -> x = Conw.nilw ``` and discarding the equality instead of substituting `x` because `x` and `Conw.nilw` are definionally equal due to proof irrelevance. @javra Do you have more complicated examples that were being affected by this issue?
27 lines
407 B
Text
27 lines
407 B
Text
case intro
|
|
n : Nat
|
|
m : Nat := n
|
|
a : Nat
|
|
e : id a = m
|
|
⊢ 0 + n = n
|
|
case intro
|
|
a : Nat
|
|
m : Nat := id a
|
|
⊢ 0 + id a = id a
|
|
case intro
|
|
n : Nat
|
|
m : Nat := n
|
|
a : Nat
|
|
e : m = id a
|
|
⊢ 0 + n = n
|
|
case intro
|
|
n : Nat
|
|
m : Nat := n
|
|
⊢ 0 + n = n
|
|
substlet.lean:25:2-25:9: error: tactic 'subst' failed, variable 'v' is a let-declaration
|
|
n : Nat
|
|
h : n = 0
|
|
m : Nat := n + 1
|
|
v : Nat := m + 1
|
|
this : v = n + 2
|
|
⊢ 0 + n = 0
|