Documentation

Init.Data.Fin.Fold

@[inline]
def Fin.foldl {α : Sort u_1} (n : Nat) (f : αFin nα) (init : α) :
α

Folds over Fin n from the left: foldl 3 f x = f (f (f x 0) 1) 2.

Equations
Instances For
    @[irreducible]
    def Fin.foldl.loop {α : Sort u_1} (n : Nat) (f : αFin nα) (x : α) (i : Nat) :
    α

    Inner loop for Fin.foldl. Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)

    Equations
    Instances For
      @[inline]
      def Fin.foldr {α : Sort u_1} (n : Nat) (f : Fin nαα) (init : α) :
      α

      Folds over Fin n from the right: foldr 3 f x = f 0 (f 1 (f 2 x)).

      Equations
      Instances For
        @[irreducible]
        def Fin.foldr.loop {α : Sort u_1} (n : Nat) (f : Fin nαα) :
        { i : Nat // i n }αα

        Inner loop for Fin.foldr. Fin.foldr.loop n f i x = f 0 (f ... (f (i-1) x))

        Equations
        Instances For