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

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

Equations

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

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

enum n is the array of all elements of Fin n in order

Equations

• Fin.enum n = Array.ofFn id

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

list n is the list of all elements of Fin n in order

Equations

• Fin.list n = (Fin.enum n).data