Stdlib.Trait.Foldable.Monomorphic
Contents
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.