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}} {A B : Type} (g : B -> A -> B) (ini : B) (ls : f A) : BSource #

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}} {A B : Type} (g : A -> B -> B) (ini : B) (ls : f A) : BSource #

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

Description

Definitions