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 = { val := min n m, isLt := ⋯ }

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

@[inline]

def Fin.foldl {α : Sort u_1} (n : Nat) (f : α → Fin n → α) (init : α) : α

Folds over Fin n from the left: foldl 3 f x = f (f (f x 0) 1) 2.

Equations

• Fin.foldl n f init = Fin.foldl.loop n f init 0

def Fin.foldl.loop {α : Sort u_1} (n : Nat) (f : α → Fin n → α) (x : α) (i : Nat) : α

Inner loop for Fin.foldl. Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)

Equations

• Fin.foldl.loop n f x i = if h : i < n then Fin.foldl.loop n f (f x { val := i, isLt := h }) (i + 1) else x

@[inline]

def Fin.foldr {α : Sort u_1} (n : Nat) (f : Fin n → α → α) (init : α) : α

Folds over Fin n from the right: foldr 3 f x = f 0 (f 1 (f 2 x)).

Equations

• Fin.foldr n f init = Fin.foldr.loop n f { val := n, property := ⋯ } init

def Fin.foldr.loop {α : Sort u_1} (n : Nat) (f : Fin n → α → α) : { i : Nat // i ≤ n } → α → α

Inner loop for Fin.foldr. Fin.foldr.loop n f i x = f 0 (f ... (f (i-1) x))

Equations

• Fin.foldr.loop n f { val := 0, property := property } x = x
• Fin.foldr.loop n f { val := Nat.succ i, property := h } x = Fin.foldr.loop n f { val := i, property := ⋯ } (f { val := i, isLt := h } x)