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

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

@[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.

@[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₀

@[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.

@[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.

@[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ₙ

@[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.

@[inline]

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

Sum of a tuple indexed by Fin n.

@[inline]

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

Product of a tuple indexed by Fin n.

@[inline]

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

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

@[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.

@[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.

@[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.

@[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.

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.

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.

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.