Description

Definitions

trait type Foldable (Container Elem : 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 : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B; syntax iterator rfor {init := 1; range := 1}; rfor : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B; }

open Foldable public

fromPolymorphicFoldable {F : Type -> Type} {{foldable : Poly.Foldable F}} {Elem} : Foldable (F Elem) ElemSource #

Make a monomorphic Foldable instance from a polymorphic one. All polymorphic types that are an instance of Poly.Foldable should use this function to create their monomorphic Foldable instance.

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

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

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