Idris2Doc : Monocle.Optional

Monocle.Optional

(source)
Definitions
record Optional : Type -> Type -> Type -> Type -> Type
  An Optional allows us to focus on a single piece of
  information in a larger data object that might or might not
  be there.
  
  An Optional is related to but less powerful than a Prism, because
  it does not allow us to directly inject a value into a larger data
  object, but only supports updating such a value if it exists.
  
  Optionals play an important role when we sequentially combine different
  types of optics: The sequential composition of a Lens with a Prism or
  vice verca results in an optional: We can no longer be certain that
  the value we focus on is still there (the Prism prevents that), nor can
  we directly inject the value into the larger data object
  (the Lens prevents that).

  Totality: total
  Visibility: public export
  Constructor: 
O : (s -> Either t a) -> ((a -> b) -> s -> t) -> Optional s t a b

  Projections:
  
.getOrModify : Optional s t a b -> s -> Either t a
  
.replace : Optional s t a b -> (a -> b) -> s -> t

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

  Totality: total
  Visibility: public export
optional : (s -> Maybe a) -> ((a -> a) -> s -> s) -> Optional' s a
  Utility constructor for monomorphic optionals.

  Totality: total
  Visibility: public export
mapA : Applicative f => Optional s t a b -> (a -> f b) -> s -> f t
  Adjust the focus sof an Optional with an effectful computation.

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

  Parameters: o
Methods:
  
toOptional : o s t a b -> Optional s t a b

Implementations:
  
ToOptional Iso
  
ToOptional Lens
  
ToOptional Optional
  
ToOptional Prism
toOptional : ToOptional o => o s t a b -> Optional s t a b
  Totality: total
  Visibility: public export
(~>) : Optional s t a b -> Optional a b c d -> Optional s t c d
  Sequential composition of Optionals.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 0
emptyO : Optional' s a
  The empty Optional, which does not focus on anything at all.

  Totality: total
  Visibility: public export
getIx : Nat -> List a -> Maybe a
  Tries to extract a value at the given index from a List.

  Totality: total
  Visibility: public export
modIx : Nat -> (a -> a) -> List a -> List a
  Modifies the value at the given index in a List.
  
  Returns the unchanged List if the index is out of bounds.

  Totality: total
  Visibility: public export
ix : Nat -> Optional' (List a) a
  An Optional focussing on the n-th element in a List.

  Totality: total
  Visibility: public export
select : (a -> Bool) -> Optional' a a
  An Optional for focussing on those values that fulfill a given
  predicate.

  Totality: total
  Visibility: public export
eqBy : Eq b => b -> (a -> b) -> Optional' a a
  An Optional for focussing on those values that are equivalent to `v`
  according to the given comparison function.

  Totality: total
  Visibility: public export
modWhere : SnocList a -> (a -> Bool) -> (a -> a) -> List a -> List a
  Totality: total
  Visibility: public export
first : (a -> Bool) -> Optional' (List a) a
  An Optional for focussing on the first value in a list
  that fulfills the given predicate.

  Totality: total
  Visibility: public export
eqFirst : Eq b => b -> (a -> b) -> Optional' (List a) a
  An Optional for focussing on the first value in a List
  that is equivalent to `v` according to the given comparison function.

  Totality: total
  Visibility: public export
stO : Applicative m => Monoid x => Optional' t s -> StateT s m x -> StateT t m x
  View a stateful computation resulting in a monoid through an
  optional.

  Totality: total
  Visibility: export