interface Foldable1 : (Type -> Type) -> Type Folds over a computation including potentially linear
mutable state.
Parameters: f
Methods:
foldl1 : (a -> e -> F1 s a) -> a -> f e -> F1 s a foldr1 : (e -> a -> F1 s a) -> a -> f e -> F1 s a foldMap1 : Monoid m => (a -> F1 s m) -> f a -> F1 s m traverse1_ : (a -> F1' s) -> f a -> F1' s
Implementations:
Foldable1 Maybe Foldable1 (Either e) Foldable1 List Foldable1 SnocList Foldable1 (Vect n) Foldable1 List1
foldl1 : Foldable1 f => (a -> e -> F1 s a) -> a -> f e -> F1 s a- Totality: total
Visibility: public export foldr1 : Foldable1 f => (e -> a -> F1 s a) -> a -> f e -> F1 s a- Totality: total
Visibility: public export foldMap1 : Foldable1 f => Monoid m => (a -> F1 s m) -> f a -> F1 s m- Totality: total
Visibility: public export traverse1_ : Foldable1 f => (a -> F1' s) -> f a -> F1' s- Totality: total
Visibility: public export for1_ : Foldable1 f => f a -> (a -> F1' s) -> F1' s Flipped version of `traverse1_`
Totality: total
Visibility: exportfoldl1List : (a -> e -> F1 s a) -> a -> List e -> F1 s a- Totality: total
Visibility: export foldr1SnocList : (e -> a -> F1 s a) -> a -> SnocList e -> F1 s a- Totality: total
Visibility: export foldr1List : (e -> a -> F1 s a) -> a -> List e -> F1 s a- Totality: total
Visibility: export foldl1SnocList : (a -> e -> F1 s a) -> a -> SnocList e -> F1 s a- Totality: total
Visibility: export foldMap1List : Monoid m => (a -> F1 s m) -> List a -> F1 s m- Totality: total
Visibility: export foldMap1SnocList : Monoid m => (a -> F1 s m) -> SnocList a -> F1 s m- Totality: total
Visibility: export traverse1_List : (a -> F1' s) -> List a -> F1' s- Totality: total
Visibility: export traverse1_SnocList : (a -> F1' s) -> SnocList a -> F1' s- Totality: total
Visibility: export foldl1Vect : (a -> e -> F1 s a) -> a -> Vect n e -> F1 s a- Totality: total
Visibility: export foldr1Vect : (e -> a -> F1 s a) -> a -> Vect n e -> F1 s a- Totality: total
Visibility: export foldMap1Vect : Monoid m => (a -> F1 s m) -> Vect n a -> F1 s m- Totality: total
Visibility: export traverse1_Vect : (a -> F1' s) -> Vect n a -> F1' s- Totality: total
Visibility: export interface Traversable1 : (Type -> Type) -> Type- Parameters: f
Constraints: Foldable1 f
Methods:
traverse1 : (a -> F1 s b) -> f a -> F1 s (f b)
Implementations:
Traversable1 Maybe Traversable1 (Either e) Traversable1 List Traversable1 SnocList Traversable1 (Vect n) Traversable1 List1
traverse1 : Traversable1 f => (a -> F1 s b) -> f a -> F1 s (f b)- Totality: total
Visibility: public export traverse1List : SnocList b -> (a -> F1 s b) -> List a -> F1 s (List b)- Totality: total
Visibility: export traverse1SnocList : List b -> (a -> F1 s b) -> SnocList a -> F1 s (SnocList b)- Totality: total
Visibility: export traverse1Vect : (sx : SnocList b) -> (a -> F1 s b) -> Vect n a -> F1 s (Vect (length sx + n) b)- Totality: total
Visibility: export for1 : Traversable1 f => f a -> (a -> F1 s b) -> F1 s (f b) Flipped version of `traverse1`
Totality: total
Visibility: exportzipWithIndex : Traversable1 f => f a -> f (Nat, a) Pairs each value in a data structure with its index of appearance.
Totality: total
Visibility: export