`GetElem?` を紹介する

[Seasawher]

GetElemがあるなら GetElem? があってもいい気がする

作れないのか？自作できるだろうか

variable {α : Type} (A : α)
/-
failed to synthesize
  GetElem? α Nat ?m.606 ?m.607
use `set_option diagnostics true` to get diagnostic information
-/
#check A[2]?

[Seasawher]

普通にある (なぜかないと勘違いした．なぜ勘違いしたかわからない...)

see: https://github.com/leanprover/lean4/blob/d4e141e233f2e54e731a2b763fbf74acf6c5d4dc/src/Init/GetElem.lean#L87

@[inherit_doc GetElem]
class GetElem? (coll : Type u) (idx : Type v) (elem : outParam (Type w))
    (valid : outParam (coll → idx → Prop)) extends GetElem coll idx elem valid where
  /--
  The syntax `arr[i]?` gets the `i`'th element of the collection `arr`,
  if it is present (and wraps it in `some`), and otherwise returns `none`.
  -/
  getElem? : coll → idx → Option elem

  /--
  The syntax `arr[i]!` gets the `i`'th element of the collection `arr`,
  if it is present, and otherwise panics at runtime and returns the `default` term
  from `Inhabited elem`.
  -/
  getElem! [Inhabited elem] (xs : coll) (i : idx) : elem :=
    match getElem? xs i with | some e => e | none => outOfBounds

export GetElem? (getElem? getElem!)

at src\lean\Init\GetElem.lean