Idris2Doc : Control.Lens.Traversal

Control.Lens.Traversal

(source)
Definitions
record IsTraversal : (Type -> Type -> Type) -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkIsTraversal : Traversing p -> IsTraversal p

  Projection: 
.runIsTraversal : IsTraversal p -> Traversing p

  Hints:
  
IsTraversal p => IsOptional p
  
IsFold p => IsTraversal p
  
IsTraversal p => IsTraversal (Indexed i p)
  
IsSetter p => IsTraversal p
.runIsTraversal : IsTraversal p -> Traversing p
  Totality: total
  Visibility: public export
runIsTraversal : IsTraversal p -> Traversing p
  Totality: total
  Visibility: public export
traversalToOptional : IsTraversal p => IsOptional p
  Totality: total
  Visibility: export
indexedTraversal : IsTraversal p => IsTraversal (Indexed i p)
  Totality: total
  Visibility: export
0 Traversal : Type -> Type -> Type -> Type -> Type
  A traversal is a lens that may have more than one focus.

  Totality: total
  Visibility: public export
0 Traversal' : Type -> Type -> Type
  `Traversal'` is the `Simple` version of `Traversal`.

  Totality: total
  Visibility: public export
0 IndexedTraversal : Type -> Type -> Type -> Type -> Type -> Type
  An indexed traversal allows access to the indices of the values as they are
  being modified.

  Totality: total
  Visibility: public export
0 IndexedTraversal' : Type -> Type -> Type -> Type
  `IndexedTraversal'` is the `Simple` version of `IndexedTraversal`.

  Totality: total
  Visibility: public export
traversal : (Applicative f => (a -> f b) -> s -> f t) -> Traversal s t a b
  Construct a traversal from a `traverse`-like function.

  Totality: total
  Visibility: public export
itraversal : (Applicative f => (i -> a -> f b) -> s -> f t) -> IndexedTraversal i s t a b
  Construct an indexed traversal from a `traverse`-like function.

  Totality: total
  Visibility: public export
iordinal : Num i => Traversal s t a b -> IndexedTraversal i s t a b
  Convert a traversal into an indexed traversal, adding an index for the
  ordinal position of the focus.

  Totality: total
  Visibility: public export
traversed : Traversable t => Traversal (t a) (t b) a b
  Derive a traversal from a `Traversable` implementation.

  Totality: total
  Visibility: public export
itraversed : Num i => Traversable t => IndexedTraversal i (t a) (t b) a b
  Derive an indexed traversal from a `Traversable` implementation.

  Totality: total
  Visibility: public export
both : Bitraversable t => Traversal (t a a) (t b b) a b
  Contstruct a traversal over a `Bitraversable` container with matching types.

  Totality: total
  Visibility: public export
backwards : Traversal s t a b -> Traversal s t a b
  Reverse the order of a traversal's focuses.

  Totality: total
  Visibility: public export
traverseOf : Applicative f => Traversal s t a b -> (a -> f b) -> s -> f t
  Map each focus of a traversal to a computation, evaluate those computations
  and combine the results.

  Totality: total
  Visibility: public export
itraverseOf : Applicative f => IndexedTraversal i s t a b -> (i -> a -> f b) -> s -> f t
  Map each focus of a traversal to a computation with acces to the index,
  evaluate those computations and combine the results.

  Totality: total
  Visibility: public export
forOf : Applicative f => Traversal s t a b -> s -> (a -> f b) -> f t
  A version of `traverseOf` but with the arguments flipped.

  Totality: total
  Visibility: public export
iforOf : Applicative f => IndexedTraversal i s t a b -> s -> (i -> a -> f b) -> f t
  A version of `itraverseOf` but with the arguments flipped.

  Totality: total
  Visibility: public export
sequenceOf : Applicative f => Traversal s t (f a) a -> s -> f t
  Evaluate each computation within the traversal and collect the results.

  Totality: total
  Visibility: public export
mapAccumLOf : Traversal s t a b -> (acc -> a -> (acc, b)) -> acc -> s -> (acc, t)
  Fold across the focuses of a traversal from the leftmost focus, providing a
  replacement value for each, and return the final accumulator along with the
  new structure.

  Totality: total
  Visibility: public export
mapAccumROf : Traversal s t a b -> (acc -> a -> (acc, b)) -> acc -> s -> (acc, t)
  Fold across the focuses of a traversal from the rightmost focus, providing a
  replacement value for each, and return the final accumulator along with the
  new structure.

  Totality: total
  Visibility: public export
scanl1Of : Traversal s t a a -> (a -> a -> a) -> s -> t
  Fold across the focuses of a traversal from the left, returning each
  intermediate value of the fold.

  Totality: total
  Visibility: public export
scanr1Of : Traversal s t a a -> (a -> a -> a) -> s -> t
  Fold across the focuses of a traversal from the right, returning each
  intermediate value of the fold.

  Totality: total
  Visibility: public export
failover : Alternative f => Traversal s t a b -> (a -> b) -> s -> f t
  Try to map over a traversal, failing if the traversal has no focuses.

  Totality: total
  Visibility: public export
ifailover : Alternative f => IndexedTraversal i s t a b -> (i -> a -> b) -> s -> f t
  Try to map over an indexed traversal, failing if the traversal has no focuses.

  Totality: total
  Visibility: public export
partsOf : Traversal s t a a -> Lens s t (List a) (List a)
  Convert a traversal into a lens over a list of values.
  
  Note that this is only a true lens if the invariant of the list's length is
  maintained. You should avoid mapping `over` this lens with a function that
  changes the list's length.

  Totality: total
  Visibility: public export
ipartsOf : IndexedTraversal i s t a a -> IndexedLens (List i) s t (List a) (List a)
  Convert an indexed traversal into an indexed lens over a list of values, with
  access to a list of indices.
  
  Note that this is only a true lens if the invariant of the list's length is
  maintained. You should avoid mapping `over` this lens with a function that
  changes the list's length.

  Totality: total
  Visibility: public export
singular : Traversal' s a -> Optional' s a
  Construct an optional that focuses on the first value of a traversal.
  
  For the fold version of this, see `pre`.

  Totality: total
  Visibility: public export
isingular : IndexedTraversal' i s a -> IndexedOptional' i s a
  Construct an indexed optional that focuses on the first value of an
  indexed traversal.
  
  For the fold version of this, see `ipre`.

  Totality: total
  Visibility: public export
elementsOf : Traversal s t a a -> (Nat -> Bool) -> Traversal s t a a
  Filter the focuses of a traversal by a predicate on their ordinal positions.

  Totality: total
  Visibility: public export
elements : Traversable t => (Nat -> Bool) -> Traversal' (t a) a
  Traverse over the elements of a `Traversable` container that satisfy a
  predicate.

  Totality: total
  Visibility: public export
elementOf : Traversal' s a -> Nat -> Optional' s a
  Construct an optional that focuses on the nth element of a traversal.

  Totality: total
  Visibility: public export
element : Traversable t => Nat -> Optional' (t a) a
  Construct an optional that focuses on the nth element of a `Traversable`
  container.

  Totality: total
  Visibility: public export
taking : Nat -> Traversal s t a a -> Traversal s t a a
  Limit a traversal to its first `n` focuses.

  Totality: total
  Visibility: public export
dropping : Nat -> Traversal s t a a -> Traversal s t a a
  Remove the first `n` focuses from a traversal.

  Totality: total
  Visibility: public export