Idris2Doc : Monocle.Setter

Monocle.Setter

(source)

Definitions

recordSetter : Type->Type->Type->Type->Type
  A Setter allows us to update zero or more values in a
larger data type.

Possible examples include updating single record fields, mapping
a function over the values in a `List` (or any other `Functor`),
or converting the characters in a string.

A Setter is parameterized over four parameters, because in general
we could not only update a value but also its type with an updating
function. Consider Setter `io`, where `s` corresponds to `IO a` and
`t` corresponds to `IO b`. Accordingly, if we have a function from
`a` to `b`, we can convert an `IO a` to an `IO b`.

Totality: total
Visibility: public export
Constructor: 
S : ((a->b) ->s->t) ->Setterstab

Projection: 
.over_ : Setterstab-> (a->b) ->s->t

Hints:
OSeqIsoSetterSetter
OSeqLensSetterSetter
OSeqPrismSetterSetter
OSeqOptionalSetterSetter
OSeqTraversalSetterSetter
OSeqSetterSetterSetter
OSeqSetterIsoSetter
OSeqSetterLensSetter
OSeqSetterPrismSetter
OSeqSetterOptionalSetter
OSeqSetterTraversalSetter
ToSetterSetter
.over_ : Setterstab-> (a->b) ->s->t
Totality: total
Visibility: public export
over_ : Setterstab-> (a->b) ->s->t
Totality: total
Visibility: public export
0Setter' : Type->Type->Type
  Convenience alias for monomorphic setters, which do not allow
us to change the value and source types.

Totality: total
Visibility: public export
interfaceToSetter : (Type->Type->Type->Type->Type) ->Type
  Interface for converting other optics to setters. With the exception
of Fold and Getter, all optics in this library have an implementation
of `ToSetter`.

Parameters: o
Methods:
toSetter : ostab->Setterstab

Implementations:
ToSetterIso
ToSetterLens
ToSetterOptional
ToSetterPrism
ToSetterSetter
ToSetterTraversal
toSetter : ToSettero=>ostab->Setterstab
Totality: total
Visibility: public export
over : ToSettero=>ostab-> (a->b) ->s->t
  Use a Setter to update the data stored in a source value.

Totality: total
Visibility: public export
set : ToSettero=>ostab->b->s->t
  Use a Setter to set the data stored in a source value.

Totality: total
Visibility: public export
(~>) : Setterstab->Setterabcd->Setterstcd
  Sequential composition of setters.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 0
map_ : Functorf=>Setter (fa) (fb) ab
  Every `Functor` gives rise to a polymorphic Setter via `map`.

Totality: total
Visibility: public export
contramap_ : Contravariantf=>Setter (fa) (fb) ba
  Every contravariant functor gives rise to a polymorphic Setter via
`contramap`.

Totality: total
Visibility: public export
overST : Monadm=>ToSettero=>ossaa-> (a->a) ->StateTsm ()
  Modify the current state with a setter

Totality: total
Visibility: export
setST : Monadm=>ToSettero=>ossaa->a->StateTsm ()
  Modify the current state with a setter

Totality: total
Visibility: export