Documentation

Batteries.Data.Fin.Basic

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

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

Equations
Instances For
    @[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.succm (α 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
    Instances For
      @[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.succm (α 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
      Instances For
        @[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
        Instances For
          @[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.castSuccm (α 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
          Instances For
            @[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.castSuccm (α 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
            Instances For
              @[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
              Instances For
                @[inline]
                def Fin.findSome? {n : Nat} {α : Type u_1} (f : Fin nOption α) :

                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
                Instances For
                  @[inline]
                  def Fin.find? {n : Nat} (p : Fin nBool) :

                  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
                  Instances For