8ebd294673
This PR fixes a `Sym.simp` panic ("unexpected kernel projection term
during simplification") that triggered when matcher iota-reduction
exposed kernel `Expr.proj` terms via struct-eta. For example, a `do`
block with a `for` loop whose state is a tuple, where `Sym.simp`
unfolds the equational lemma and then descends into a destructuring
match.
19 lines
370 B
Text
19 lines
370 B
Text
import Lean
|
|
|
|
set_option linter.unusedVariables false in
|
|
def loopy : Option Nat := do
|
|
let mut x : Nat := 0
|
|
let mut y : Nat := 0
|
|
let mut ok : Bool := false
|
|
for _ in [:1] do
|
|
x := x + 1
|
|
y := y + 1
|
|
ok := true
|
|
return x
|
|
|
|
/-- warning: declaration uses `sorry` -/
|
|
#guard_msgs in
|
|
example : loopy = some 0 := by
|
|
sym =>
|
|
simp [loopy.eq_1]
|
|
sorry
|