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, ⋯⟩

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).toList

@[inline]

def Fin.foldlM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (n : Nat) (f : α → Fin n → m α) (init : α) : m α

Folds a monadic function over Fin n from left to right:

Fin.foldlM n f x₀ = do
  let x₁ ← f x₀ 0
  let x₂ ← f x₁ 1
  ...
  let xₙ ← f xₙ₋₁ (n-1)
  pure xₙ

Equations

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

@[irreducible]

def Fin.foldlM.loop {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (n : Nat) (f : α → Fin n → m α) (x : α) (i : Nat) : m α

Inner loop for Fin.foldlM.

Fin.foldlM.loop n f xᵢ i = do
  let xᵢ₊₁ ← f xᵢ i
  ...
  let xₙ ← f xₙ₋₁ (n-1)
  pure xₙ

Equations

• Fin.foldlM.loop n f x i = if h : i < n then do let x ← f x ⟨i, h⟩ Fin.foldlM.loop n f x (i + 1) else pure x

@[inline]

def Fin.foldrM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (n : Nat) (f : Fin n → α → m α) (init : α) : m α

Folds a monadic function over Fin n from right to left:

Fin.foldrM n f xₙ = do
  let xₙ₋₁ ← f (n-1) xₙ
  let xₙ₋₂ ← f (n-2) xₙ₋₁
  ...
  let x₀ ← f 0 x₁
  pure x₀

Equations

• Fin.foldrM n f init = Fin.foldrM.loop n f ⟨n, ⋯⟩ init

@[irreducible]

def Fin.foldrM.loop {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (n : Nat) (f : Fin n → α → m α) : { i : Nat // i ≤ n } → α → m α

Inner loop for Fin.foldrM.

Fin.foldrM.loop n f i xᵢ = do
  let xᵢ₋₁ ← f (i-1) xᵢ
  ...
  let x₁ ← f 1 x₂
  let x₀ ← f 0 x₁
  pure x₀

Equations

• Fin.foldrM.loop n f ⟨0, property⟩ x = pure x
• Fin.foldrM.loop n f ⟨i.succ, h⟩ x = f ⟨i, h⟩ x >>= Fin.foldrM.loop n f ⟨i, ⋯⟩