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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
@[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)

Instances For

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

Instances For

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

Instances For

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

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

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

Instances For

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

Instances For

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

Instances For