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

@[inline]

def Fin.dfoldrM {m : Type u_1 → Type u_2} [Monad m] (n : Nat) (α : Fin (n + 1) → Type u_1) (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (init : α (last n)) : m (α 0)

Heterogeneous monadic fold over Fin n from right to left:

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

This is the dependent version of Fin.foldrM.

Equations

• Fin.dfoldrM n α f init = Fin.dfoldrM.loop n α f n ⋯ init

@[specialize #[]]

def Fin.dfoldrM.loop {m : Type u_1 → Type u_2} [Monad m] (n : Nat) (α : Fin (n + 1) → Type u_1) (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α 0)

Inner loop for Fin.dfoldrM.

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

Equations

• Fin.dfoldrM.loop n α f i_2.succ h_2 x_2 = f ⟨i_2, ⋯⟩ x_2 >>= Fin.dfoldrM.loop n α f i_2 ⋯
• Fin.dfoldrM.loop n α f 0 h_2 x_2 = pure x_2

@[inline]

def Fin.dfoldr (n : Nat) (α : Fin (n + 1) → Type u_1) (f : (i : Fin n) → α i.succ → α i.castSucc) (init : α (last n)) : α 0

Heterogeneous fold over Fin n from the right: foldr 3 f x = f 0 (f 1 (f 2 x)), where f 2 : α 3 → α 2, f 1 : α 2 → α 1, etc.

This is the dependent version of Fin.foldr.

Equations

• Fin.dfoldr n α f init = Fin.dfoldrM n α f init

@[inline]

def Fin.dfoldlM {m : Type u_1 → Type u_2} [Monad m] (n : Nat) (α : Fin (n + 1) → Type u_1) (f : (i : Fin n) → α i.castSucc → m (α i.succ)) (init : α 0) : m (α (last n))

Heterogeneous monadic fold over Fin n from left to right:

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

This is the dependent version of Fin.foldlM.

Equations

• Fin.dfoldlM n α f init = Fin.dfoldlM.loop n α f 0 ⋯ init

@[irreducible, specialize #[]]

def Fin.dfoldlM.loop {m : Type u_1 → Type u_2} [Monad m] (n : Nat) (α : Fin (n + 1) → Type u_1) (f : (i : Fin n) → α i.castSucc → m (α i.succ)) (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α (last n))

Inner loop for Fin.dfoldlM.

Fin.foldM.loop n α f i h xᵢ = do
let xᵢ₊₁ : α (i+1) ← f i xᵢ
...
let xₙ : α n ← f (n-1) xₙ₋₁
pure xₙ

Equations

• Fin.dfoldlM.loop n α f i h x = if h' : i < n then f ⟨i, h'⟩ x >>= Fin.dfoldlM.loop n α f (i + 1) ⋯ else cast ⋯ (pure x)

@[inline]

def Fin.dfoldl (n : Nat) (α : Fin (n + 1) → Type u_1) (f : (i : Fin n) → α i.castSucc → α i.succ) (init : α 0) : α (last n)

Heterogeneous fold over Fin n from the left: foldl 3 f x = f 0 (f 1 (f 2 x)), where f 0 : α 0 → α 1, f 1 : α 1 → α 2, etc.

This is the dependent version of Fin.foldl.

Equations

• Fin.dfoldl n α f init = Fin.dfoldlM n α f init

@[inline]

def Fin.sum {α : Type u_1} {n : Nat} [Zero α] [Add α] (x : Fin n → α) : α

Sum of a tuple indexed by Fin n.

Equations

• Fin.sum x = Fin.foldr n (fun (x1 : Fin n) (x2 : α) => x x1 + x2) 0

@[inline]

def Fin.prod {α : Type u_1} {n : Nat} [One α] [Mul α] (x : Fin n → α) : α

Product of a tuple indexed by Fin n.

Equations

• Fin.prod x = Fin.foldr n (fun (x1 : Fin n) (x2 : α) => x x1 * x2) 1

@[inline]

def Fin.countP {n : Nat} (p : Fin n → Bool) : Nat

Count the number of true values of a decidable predicate on Fin n.

Equations

• Fin.countP p = Fin.sum fun (x : Fin n) => (p x).toNat

@[inline]

def Fin.findSome? {n : Nat} {α : Type u_1} (f : Fin n → Option α) : Option α

findSome? f returns f i for the first i for which f i is some _, or none if no such element is found. The function f is not evaluated on further inputs after the first i is found.

Equations

• Fin.findSome? f = Fin.foldl n (fun (r : Option α) (i : Fin n) => r <|> f i) none

@[inline]

def Fin.findSomeRev? {n : Nat} {α : Type u_1} (f : Fin n → Option α) : Option α

findSomeRev? f returns f i for the last i for which f i is some _, or none if no such element is found. The function f is not evaluated on further inputs after the first i is found.

Equations

• Fin.findSomeRev? f = Fin.findSome? fun (x : Fin n) => f x.rev

@[reducible, inline]

abbrev Fin.find? {n : Nat} (p : Fin n → Bool) : Option (Fin n)

find? p returns the first i for which p i = true, or none if no such element is found. The function p is not evaluated on further inputs after the first i is found.

Equations

• Fin.find? p = Fin.findSome? (Option.guard p)

@[reducible, inline]

abbrev Fin.findRev? {n : Nat} (p : Fin n → Bool) : Option (Fin n)

find? p returns the first i for which p i = true, or none if no such element is found. The function p is not evaluated on further inputs after the first i is found.

Equations

• Fin.findRev? p = Fin.findSomeRev? (Option.guard p)

def Fin.divNat {m n : Nat} (i : Fin (m * n)) : Fin m

Compute i / n, where n is a Nat and inferred the type of i.

Equations

• i.divNat = ⟨↑i / n, ⋯⟩

def Fin.modNat {m n : Nat} (i : Fin (m * n)) : Fin n

Compute i % n, where n is a Nat and inferred the type of i.

Equations

• i.modNat = ⟨↑i % n, ⋯⟩

def Fin.mkDivMod {m n : Nat} (i : Fin m) (j : Fin n) : Fin (m * n)

Compute the element of Fin (m * n) with quotient i : Fin m and remainder j : Fin n when divided by n.

Equations

• i.mkDivMod j = ⟨n * ↑i + ↑j, ⋯⟩