型クラスのインスタンスをローカルに作る例

ローカルに型クラス C の項を作ると、勝手に [instance] 属性が付与されたことになるらしく、そのままインスタンスが生成される。

/-- リストの最小値をそのインデックスと共に出力する -/
def List.minIdx? {α : Type} [Ord α] (xs : List α) : Option (Nat × α) :=
  loop xs 0
where
  loop : List α → Nat → Option (Nat × α)
  | [], _ => none
  | x :: xs, i =>
    match loop xs (i + 1) with
    | none => some (i, x)
    | some (j, y) =>
      let _ : LT α := ltOfOrd
      if x < y then (i, x) else some (j, y)

#guard List.minIdx? [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5] = some (3, 1)

Start with the local LT α declaration in the issue's List.minIdx? example and the accompanying #guard. Verify the observed behavior for a locally created type-class term, then document the example and its explanation; the issue is complete when the behavior is clearly demonstrated for readers.