def Fin.clamp (n m : Nat) : Fin (m + 1)

min n m as an element of Fin (m + 1)

Equations

• Fin.clamp n m = ⟨min n m, ⋯⟩

@[deprecated Array.finRange]

def Fin.enum (n : Nat) : Array (Fin n)

Alias of Array.finRange.

---

finRange n is the array of all elements of Fin n in order.

Equations

• Fin.enum = Array.finRange

@[deprecated List.finRange]

def Fin.list (n : Nat) : List (Fin n)

Alias of List.finRange.

---

finRange n lists all elements of Fin n in order

Equations

• Fin.list = List.finRange