Idris2Doc : Monocle.Traversal

Monocle.Traversal

(source)
Definitions
record Traversal : Type -> Type -> Type -> Type -> Type
  A Traversal is the most basic optic unifying a Fold and a Setter.
  
  While an Optional can focus on at most one value, at Traversal
  can focus on many values at once. This makes it very useful for
  large-scale modifications of many values in a data object.

  Totality: total
  Visibility: public export
  Constructor: 
T : (Applicative f => (a -> f b) -> s -> f t) -> Fold s t a b -> Setter s t a b -> Traversal s t a b

  Projections:
  
.fold_ : Traversal s t a b -> Fold s t a b
  
.mapA : Traversal s t a b -> Applicative f => (a -> f b) -> s -> f t
  
.set_ : Traversal s t a b -> Setter s t a b

  Hints:
  
OSeq Iso Traversal Traversal
  
OSeq Lens Traversal Traversal
  
OSeq Prism Traversal Traversal
  
OSeq Optional Traversal Traversal
  
OSeq Traversal Traversal Traversal
  
OSeq Traversal Iso Traversal
  
OSeq Traversal Lens Traversal
  
OSeq Traversal Prism Traversal
  
OSeq Traversal Optional Traversal
  
OSeq Traversal Getter Fold
  
OSeq Traversal Setter Setter
  
OSeq Traversal Fold Fold
  
OSeq Setter Traversal Setter
  
OSeq Getter Traversal Fold
  
OSeq Fold Traversal Fold
  
ToFold Traversal
  
ToSetter Traversal
  
ToTraversal Traversal
.mapA : Traversal s t a b -> Applicative f => (a -> f b) -> s -> f t
  Totality: total
  Visibility: public export
mapA : Traversal s t a b -> Applicative f => (a -> f b) -> s -> f t
  Totality: total
  Visibility: public export
.fold_ : Traversal s t a b -> Fold s t a b
  Totality: total
  Visibility: public export
fold_ : Traversal s t a b -> Fold s t a b
  Totality: total
  Visibility: public export
.set_ : Traversal s t a b -> Setter s t a b
  Totality: total
  Visibility: public export
set_ : Traversal s t a b -> Setter s t a b
  Totality: total
  Visibility: public export
0 Traversal' : Type -> Type -> Type
  Convenience alias for monomorphic Traversals, which do not allow
  us to change the value and source types.

  Totality: total
  Visibility: public export
interface ToTraversal : (Type -> Type -> Type -> Type -> Type) -> Type
  Interface for converting other optics to Traversals.

  Parameters: o
Methods:
  
toTraversal : o s t a b -> Traversal s t a b

Implementations:
  
ToTraversal Iso
  
ToTraversal Lens
  
ToTraversal Optional
  
ToTraversal Prism
  
ToTraversal Traversal
toTraversal : ToTraversal o => o s t a b -> Traversal s t a b
  Totality: total
  Visibility: public export
(~>) : Traversal s t a b -> Traversal a b c d -> Traversal s t c d
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 0
modifyA : ToTraversal l => Applicative f => l s t a b -> (a -> f b) -> s -> f t
  Adjust the focus of a Traversal with an effectful computation.

  Totality: total
  Visibility: export
traverse_ : Traversable f => Traversal (f a) (f b) a b
  Every `Traversable` trivially gives rise to a Traversal.

  Totality: total
  Visibility: public export
list_ : Traversal (List a) (List b) a b
  `traverse_` specialized to lists.

  Totality: total
  Visibility: public export
snoclist_ : Traversal (SnocList a) (SnocList b) a b
  `traverse_` specialized to snoclists.

  Totality: total
  Visibility: public export
list1_ : Traversal (List1 a) (List1 b) a b
  `traverse_` specialized to non-empty lists.

  Totality: total
  Visibility: public export
vect_ : Traversal (Vect n a) (Vect n b) a b
  `traverse_` specialized to vectors.

  Totality: total
  Visibility: public export