blob: 7132eb92e2715a0eff153521cdc1228c5f6ea49d [file] [edit]
invalidPatternIssue.lean:13:0-13:20: error: invalid patterns, `x` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
{ pred := Nat.succ .(x.1) }