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

foldr {container elem : Type} {{Foldable container elem}} {B : Type} (g : elem -> B -> B) : B -> container -> BSource #

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