Stdlib.Trait.Foldable.Polymorphic

Contents

trait type Foldable (F : Type -> Type)Source #

A trait for combining elements into a single result, processing one element at a time.

Constructors

| mkFoldable@{ syntax iterator for {init := 1; range := 1}; for : {A B : Type} -> (B -> A -> B) -> B -> F A -> B; syntax iterator rfor {init := 1; range := 1}; rfor : {A B : Type} -> (B -> A -> B) -> B -> F A -> B; }

open Foldable public

foldl {F : Type -> Type} {{Foldable F}} {Elem Acc : Type} (fun : Acc -> Elem -> Acc) (initialValue : Acc) (container : F Elem) : AccSource #

Combine the elements of the type using the provided function starting with the element in the left-most position.

foldr {F : Type -> Type} {{Foldable F}} {Elem Acc : Type} (fun : Elem -> Acc -> Acc) (initialValue : Acc) (container : F Elem) : AccSource #

Combine the elements of the type using the provided function starting with the element in the right-most position.

Description

Definitions