Idris2Doc : Monocle.Lens

Monocle.Lens

(source)
Definitions
record Lens : Type -> Type -> Type -> Type -> Type
  A Lens unifies a `Setter` and a Getter, and is therefore typically used
  to focus on a single value in a larger data type.
  
  Lenses are best known for allowing us to extract and update record fields,
  but they can also be used with other types of data.
  
  A Lens is parameterized over four parameters, because in general
  we could not only update a value but also its type with an updating
  function. Consider Lens `fst`, where `s` corresponds to `(a,c)` and
  `t` corresponds to `(b,c)`. Accordingly, if we have a function from
  `a` to `b`, we can convert a pair of type `(a,c)` to one of type `(b,c)`.

  Totality: total
  Visibility: public export
  Constructor: 
L : (s -> a) -> ((a -> b) -> s -> t) -> Lens s t a b

  Projections:
  
.get_ : Lens s t a b -> s -> a
  
.mod_ : Lens s t a b -> (a -> b) -> s -> t

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

  Totality: total
  Visibility: public export
lens : (s -> a) -> (b -> s -> t) -> Lens s t a b
  Alternative constructor for creating a Lens from a getting and
  a setting function.

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

  Parameters: o
Methods:
  
toLens : o s t a b -> Lens s t a b

Implementations:
  
ToLens Iso
  
ToLens Lens
toLens : ToLens o => o s t a b -> Lens s t a b
  Totality: total
  Visibility: public export
setL : Lens s t a b -> b -> s -> t
  Specialized version of `set` that sometimes helps with type inference.

  Totality: total
  Visibility: public export
modF : Functor f => Lens s t a b -> (a -> f b) -> s -> f t
  Modify the value focussed on by the given Lens with an effectful
  computation.

  Totality: total
  Visibility: public export
(~>) : Lens s t x y -> Lens x y a b -> Lens s t a b
  Sequential composition of lenses.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 0
fst : Lens (a, c) (b, c) a b
  A Lens focussing on the first element of a pair.

  Totality: total
  Visibility: public export
snd : Lens (c, a) (c, b) a b
  A Lens focussing on the second element of a pair.

  Totality: total
  Visibility: public export
head : Lens' (Vect (S n) a) a
  A Lens focussing on the head of a non-empty vector.

  Totality: total
  Visibility: public export
tail : Lens' (Vect (S n) a) (Vect n a)
  A Lens focussing on the tail of a non-empty vector.

  Totality: total
  Visibility: public export
ix : Fin n -> Lens' (Vect n a) a
  A Lens focussing on a specific element in a vector.

  Totality: total
  Visibility: public export
head1 : Lens' (List1 a) a
  A Lens focussing on the head of a non-empty list.

  Totality: total
  Visibility: public export
tail1 : Lens' (List1 a) (List a)
  A Lens focussing on the tail of a non-empty list.

  Totality: total
  Visibility: public export
at : Ord k => k -> Lens' (SortedMap k v) (Maybe v)
  A Lens focussing on the value associated with the given
  key in a `SortedMap`.
  
  Note: Unlike a related `Optional`, which we get via `at k .> just`,
        this Lens allows us to remove a key from a dictionary by
        setting the corresponding value to `Nothing`.

  Totality: total
  Visibility: public export
atDflt : Ord k => k -> v -> Lens' (SortedMap k v) v
  Like `at` but yields the given default value in case no
  value has been associated with the given key.

  Totality: total
  Visibility: export
atAuto : Ord k => k -> v => Lens' (SortedMap k v) v
  Like `atDflt` but using an auto-implicit argument for the default
  value.

  Totality: total
  Visibility: export
allGet : Elem t ks => All f ks -> f t
  Totality: total
  Visibility: public export
allUpd : Elem t ks => (f t -> f t) -> All f ks -> All f ks
  Totality: total
  Visibility: public export
prod : (0 t : k) -> Elem t ks => Lens' (All f ks) (f t)
  Lens focussing on a single element in a heterogeneous list.

  Totality: total
  Visibility: public export
allHead : Lens' (All f (k :: ks)) (f k)
  Totality: total
  Visibility: public export
allTail : Lens' (All f (k :: ks)) (All f ks)
  Totality: total
  Visibility: public export
stL : Functor m => Lens' t s -> StateT s m x -> StateT t m x
  View a state through a lens

  Totality: total
  Visibility: export