match 用に専用のラッパーを作る例 (match 式の融通の利かなさを何とかする例)

lean-ja における Yuki さんの投稿から。

namespace String

@[ext]
structure ValidPosPlusOne (s : String) where
  offset : Pos.Raw
  isValidOrPlusOne : offset.IsValid s ∨ offset = s.rawEndPos.offsetBy ⟨1⟩

inductive ValidPosPlusOne' (s : String) : Type where
| validPos (p : ValidPos s) : ValidPosPlusOne' s
| sentinel : ValidPosPlusOne' s

#check ValidPosPlusOne.mk
#check ValidPosPlusOne'.sentinel

def wrap (s : String) (p : ValidPosPlusOne s) : ValidPosPlusOne' s := by
  by_cases h : p.offset = s.rawEndPos.offsetBy ⟨1⟩
  exact ValidPosPlusOne'.sentinel
  have h' : p.offset.IsValid s := by
    cases p.isValidOrPlusOne with
    | inl h => exact h
    | inr h => contradiction
  exact ValidPosPlusOne'.validPos ⟨ p.offset, h' ⟩

namespace ValidPosPlusOne

variable {s : String}

example {s : String} (p : ValidPosPlusOne s) (p' := wrap s p) : Nat :=
  match p' with
  | .validPos pos => 1 -- It works!
  | .sentinel => 2

end ValidPosPlusOne

No file or test is named. Start by locating where comparable Lean examples are kept, then use the wrapper example in the issue as the reference. Done means the repository includes a clear example showing how the dedicated wrapper makes the match expression work.