Control.Lens.Fold

Definitions

record IsFold : (Type -> Type -> Type) -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsFold : (Traversing p, Bicontravariant p) -> IsFold p

Projection: 

.runIsFold : IsFold p -> (Traversing p, Bicontravariant p)

Hints:

IsFold p => IsOptFold p

IsFold p => IsTraversal p

.runIsFold : IsFold p -> (Traversing p, Bicontravariant p)

Totality: total
Visibility: public export

runIsFold : IsFold p -> (Traversing p, Bicontravariant p)

Totality: total
Visibility: public export

foldToOptFold : IsFold p => IsOptFold p

Totality: total
Visibility: export

foldToTraversal : IsFold p => IsTraversal p

Totality: total
Visibility: export

0 Fold : Type -> Type -> Type

  A fold is a getter that accesses multiple focus elements.
  `Fold s a` is equivalent to `s -> List a`.

Totality: total
Visibility: public export

0 IndexedFold : Type -> Type -> Type -> Type

  An indexed fold returns indices while getting.

Totality: total
Visibility: public export

folded : Foldable f => Fold (f a) a

  Derive a fold from a `Foldable` implementation.

Totality: total
Visibility: public export

unfolded : (s -> Maybe (a, s)) -> Fold s a

  Construct a fold from an unfolding function.
  
  This function is not total, as it may result in an infinite amount
  of focuses.

Visibility: public export

folding : Foldable f => (s -> f a) -> Fold s a

  Construct a fold from a function into a foldable container.

Totality: total
Visibility: public export

ifolding : Foldable f => (s -> f (i, a)) -> IndexedFold i s a

  Construct an indexed fold from a function into a foldable container.

Totality: total
Visibility: public export

backwards : Fold s a -> Fold s a

  Reverse the order of a fold's focuses.

Totality: total
Visibility: public export

replicated : Nat -> Fold a a

  Construct a fold that replicates the input n times.

Totality: total
Visibility: public export

foldMapOf : Monoid m => Fold s a -> (a -> m) -> s -> m

  Map each focus of an optic to a monoid value and combine them.

Totality: total
Visibility: public export

ifoldMapOf : Monoid m => IndexedFold i s a -> (i -> a -> m) -> s -> m

  Map each focus of an optic to a monoid value with access to the index and
  combine them.

Totality: total
Visibility: public export

foldrOf : Fold s a -> (a -> acc -> acc) -> acc -> s -> acc

  Combine the focuses of an optic using the provided function, starting from
  the right.

Totality: total
Visibility: public export

ifoldrOf : IndexedFold i s a -> (i -> a -> acc -> acc) -> acc -> s -> acc

  Combine the focuses of an optic using the provided function with access to
  the index, starting from the right.

Totality: total
Visibility: public export

foldlOf : Fold s a -> (acc -> a -> acc) -> acc -> s -> acc

  Combine the focuses of an optic using the provided function, starting from
  the left.

Totality: total
Visibility: public export

ifoldlOf : IndexedFold i s a -> (i -> acc -> a -> acc) -> acc -> s -> acc

  Combine the focuses of an optic using the provided function with access to
  the index, starting from the left.

Totality: total
Visibility: public export

concatOf : Monoid m => Fold s m -> s -> m

  Combine each focus value of an optic using a monoid structure.

Totality: total
Visibility: public export

choiceOf : Alternative f => Fold s (Lazy (f a)) -> s -> f a

  Fold over the focuses of an optic using Alternative.

Totality: total
Visibility: public export

sequenceOf_ : Applicative f => Fold s (f a) -> s -> f ()

  Evaluate each computation of an optic and discard the results.

Totality: total
Visibility: public export

traverseOf_ : Applicative f => Fold s a -> (a -> f b) -> s -> f ()

  Map each focus of an optic to a computation, evaluate those
  computations and discard the results.

Totality: total
Visibility: public export

itraverseOf_ : Applicative f => IndexedFold i s a -> (i -> a -> f b) -> s -> f ()

  Map each focus of an optic to a computation with access to the index,
  evaluate those computations and discard the results.

Totality: total
Visibility: public export

forOf_ : Applicative f => Fold s a -> s -> (a -> f b) -> f ()

  A version of `traverseOf_` with the arguments flipped.

Totality: total
Visibility: public export

iforOf_ : Applicative f => IndexedFold i s a -> s -> (i -> a -> f b) -> f ()

  A version of `itraverseOf_` with the arguments flipped.

Totality: total
Visibility: public export

andOf : Fold s (Lazy Bool) -> s -> Bool

  The conjunction of an optic containing lazy boolean values.

Totality: total
Visibility: public export

orOf : Fold s (Lazy Bool) -> s -> Bool

  The disjunction of an optic containing lazy boolean values.

Totality: total
Visibility: public export

allOf : Fold s a -> (a -> Bool) -> s -> Bool

  Return `True` if all focuses of the optic satisfy the predicate.

Totality: total
Visibility: public export

iallOf : IndexedFold i s a -> (i -> a -> Bool) -> s -> Bool

  Return `True` if all focuses of the indexed optic satisfy the predicate.

Totality: total
Visibility: public export

anyOf : Fold s a -> (a -> Bool) -> s -> Bool

  Return `True` if any focuses of the optic satisfy the predicate.

Totality: total
Visibility: public export

ianyOf : IndexedFold i s a -> (i -> a -> Bool) -> s -> Bool

  Return `True` if any focuses of the indexed optic satisfy the predicate.

Totality: total
Visibility: public export

elemOf : Eq a => Fold s a -> a -> s -> Bool

  Return `True` if the element occurs in the focuses of the optic.

Totality: total
Visibility: public export

lengthOf : Fold s a -> s -> Nat

  Calculate the number of focuses of the optic.

Totality: total
Visibility: public export

firstOf : Fold s a -> s -> Maybe a

  Access the first focus value of an optic, returning `Nothing` if there are
  no focuses.
  
  This is identical to `preview`.

Totality: total
Visibility: public export

ifirstOf : IndexedFold i s a -> s -> Maybe (i, a)

  Access the first focus value and index of an indexed optic, returning Nothing
  if there are no focuses.
  
  This is identical to `ipreview`.

Totality: total
Visibility: public export

lastOf : Fold s a -> s -> Maybe a

  Access the last focus value of an optic, returning `Nothing` if there are
  no focuses.

Totality: total
Visibility: public export

ilastOf : IndexedFold i s a -> s -> Maybe (i, a)

  Access the last focus value and index of an indexed optic, returning Nothing
  if there are no focuses.

Totality: total
Visibility: public export

has : Fold s a -> s -> Bool

  Return `True` if the optic focuses on any values.

Totality: total
Visibility: public export

hasn't : Fold s a -> s -> Bool

  Return `True` if the optic does not focus on any values.

Totality: total
Visibility: public export

previews : Fold s a -> (a -> r) -> s -> Maybe r

  Access the first focus value of an optic and apply a function to it,
  returning `Nothing` if there are no focuses.

Totality: total
Visibility: public export

preview : Fold s a -> s -> Maybe a

  Access the first focus value of an optic, returning `Nothing` if there are
  no focuses.
  
  This is an alias for `firstOf`.

Totality: total
Visibility: public export

(^?) : s -> Fold s a -> Maybe a

  Access the first focus value of an optic, returning `Nothing` if there are
  no focuses.
  
  This is the operator form of `preview`.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

ipreview : IndexedFold i s a -> s -> Maybe (i, a)

  Access the first focus value and index of an indexed optic, returning Nothing
  if there are no focuses.
  
  This is an alias for `ifirstOf`.

Totality: total
Visibility: public export

(^@?) : s -> IndexedFold i s a -> Maybe (i, a)

  Access the first focus value and index of an indexed optic, returning Nothing
  if there are no focuses.
  
  This is the operator form of `ipreview`.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

pre : Fold s a -> OptionalFold s a

  Convert a `Fold` into an `OptionalFold` that accesses the first focus element.
  
  For the traversal version of this, see `singular`.

Totality: total
Visibility: public export

ipre : IndexedFold i s a -> IndexedOptionalFold i s a

  Convert an `IndexedFold` into an `IndexedOptionalFold` that accesses the
  first focus element.
  
  For the traversal version of this, see `isingular`.

Totality: total
Visibility: public export

toListOf : Fold s a -> s -> List a

  Return a list of all focuses of a fold.

Totality: total
Visibility: public export

(^..) : s -> Fold s a -> List a

  Return a list of all focuses of a fold.
  
  This is the operator form of `toListOf`.

Totality: total
Visibility: public export

itoListOf : IndexedFold i s a -> s -> List (i, a)

  Return a list of all focuses and indices of an indexed fold.

Totality: total
Visibility: public export

(^@..) : s -> IndexedFold i s a -> List (i, a)

  Return a list of all focuses and indices of an indexed fold.
  
  This is the operator form of `itoListOf`.

Totality: total
Visibility: public export