List α の要素を Std.Range を使って範囲取得する

まずは関数として作ってみようということで、これが試作品

疑問：

• 指定された Range が List.length からはみ出ているときに、「取れるだけ取る」のか、それともエラーや none として返すのかで方針が分かれうることに気が付いた。

universe u

def List.getRange {α : Type u} (l : List α) (range : Std.Range)
    (valid : range.stop < l.length := by get_elem_tactic) : List α := Id.run do
  let mut result := []
  for h : i in range do
    result := (
      have : i < l.length := by
        dsimp [Membership.mem] at h
        omega
      l.get ⟨i, this⟩ :: result
    )
  return result.reverse

def List.getRange! {α : Type u} [Inhabited α] (l : List α) (range : Std.Range) : List α := Id.run do
  let mut result := []
  for i in range do
    result := l.get! i :: result
  return result.reverse

def List.getRange? {α : Type u} (l : List α) (range : Std.Range) : Option (List α) := do
  let mut result := []
  for i in range do
    let a ← l.get? i
    result := a :: result
  return result.reverse

#guard [1, 2, 3, 4, 5].getRange [0 : 2] = [1, 2]

#guard [1, 2, 3, 4, 5].getRange! [0 : 4] = [1, 2, 3, 4]

#guard [1, 2, 3, 4, 5].getRange? [0 : 4] = some [1, 2, 3, 4]

#guard [1, 2, 3, 4, 5].getRange? [2 : 6] = none

Start from the prototype definitions and #guard examples in the issue, focusing on how the proposed getRange, getRange!, and getRange? variants handle ranges beyond List.length. Resolve whether out-of-bounds ranges should truncate, fail, or return none, then document the decision with corresponding examples and tests.