Idris2Doc : Control.Lens.Setter

Control.Lens.Setter

(source)

Definitions

record IsSetter : (Type -> Type -> Type) -> Type
Totality: total
Visibility: public export
Constructor: 
MkIsSetter : Mapping p -> IsSetter p

Projection: 
.runIsSetter : IsSetter p -> Mapping p

Hints:
IsSetter p => IsSetter (Indexed i p)
IsSetter p => IsTraversal p
.runIsSetter : IsSetter p -> Mapping p
Totality: total
Visibility: public export
runIsSetter : IsSetter p -> Mapping p
Totality: total
Visibility: public export
setterToTraversal : IsSetter p => IsTraversal p
Totality: total
Visibility: export
indexedSetter : IsSetter p => IsSetter (Indexed i p)
Totality: total
Visibility: export
0 Setter : Type -> Type -> Type -> Type -> Type
  A setter is an optic that only supports setting, not getting.

More specifically, a setter can modify zero or more focus elements. This
means that all traversals are setters.

Setters can be thought of as a generalization of the `Functor` interface,
allowing one to map over the contents of a structure.

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

Totality: total
Visibility: public export
0 IndexedSetter : Type -> Type -> Type -> Type -> Type -> Type
  An indexed setter allows access to an index while setting.

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

Totality: total
Visibility: public export
sets : ((a -> b) -> s -> t) -> Setter s t a b
  Construct a setter from a modifying function.

Totality: total
Visibility: public export
isets : ((i -> a -> b) -> s -> t) -> IndexedSetter i s t a b
  Construct an indexed setter from a modifying function.

Totality: total
Visibility: public export
mapped : Functor f => Setter (f a) (f b) a b
  Derive a setter from a `Functor` implementation.

Totality: total
Visibility: public export
contramapped : Contravariant f => Setter (f a) (f b) b a
  Derive a setter from a `Contravariant` implementation.

Totality: total
Visibility: public export
over : Setter s t a b -> (a -> b) -> s -> t
  Modify the focus or focuses of an optic.

Totality: total
Visibility: public export
(%~) : Setter s t a b -> (a -> b) -> s -> t
  Modify the focus or focuses of an optic.

This is the operator form of `over`.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
iover : IndexedSetter i s t a b -> (i -> a -> b) -> s -> t
  Modify the focus or focuses of an indexed optic, having access to the index.

Totality: total
Visibility: public export
(%@~) : IndexedSetter i s t a b -> (i -> a -> b) -> s -> t
  Modify the focus or focuses of an indexed optic, having access to the index.

This is the operator form of `iover`.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
set : Setter s t a b -> b -> s -> t
  Set the focus or focuses of an optic to a constant value.

Totality: total
Visibility: public export
(.~) : Setter s t a b -> b -> s -> t
  Set the focus or focuses of an optic to a constant value.

This is the operator form of `set`.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
iset : IndexedSetter i s t a b -> (i -> b) -> s -> t
  Set the focus or focuses of an indexed optic, having access to the index.

Totality: total
Visibility: public export
(.@~) : IndexedSetter i s t a b -> (i -> b) -> s -> t
  Set the focus or focuses of an indexed optic, having access to the index.

This is the operator form of `iset`.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
(?~) : Setter s t a (Maybe b) -> b -> s -> t
  Set the focus of an optic to `Just` a value.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
(<.~) : Setter s t a b -> b -> s -> (b, t)
  Set a value with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
(<?~) : Setter s t a (Maybe b) -> b -> s -> (b, t)
  Set `Just` a value with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
(+~) : Num a => Setter s t a a -> a -> s -> t
  Add a constant value to the focus of an optic.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
(*~) : Num a => Setter s t a a -> a -> s -> t
  Multiply the focus of an optic by a constant value.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
(-~) : Neg a => Setter s t a a -> a -> s -> t
  Subtract a constant value from the focus of an optic.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
(/~) : Fractional a => Setter s t a a -> a -> s -> t
  Divide the focus of an optic by a constant value.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
(||~) : Setter s t Bool Bool -> Lazy Bool -> s -> t
  Logically OR the focus of an optic with a constant value.

Like `(||)`, this operator takes a lazy second argument.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
(&&~) : Setter s t Bool Bool -> Lazy Bool -> s -> t
  Logically AND the focus of an optic with a constant value.

Like `(&&)`, this operator takes a lazy second argument.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
(<+>~) : Semigroup a => Setter s t a a -> a -> s -> t
  Modify the focus of an optic using the semigroup/monoid operator.

The constant value is applied to the focus from the right:
```idris
l <+>~ x = over l (<+> x)
```

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
(%=) : MonadState s m => Setter s s a b -> (a -> b) -> m ()
  Modify the focus of an optic within a state monad.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(%@=) : MonadState s m => IndexedSetter i s s a b -> (i -> a -> b) -> m ()
  Modify the focus of an optic within a state monad, having access to the index.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(.=) : MonadState s m => Setter s s a b -> b -> m ()
  Set the focus of an optic within a state monad.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(.@=) : MonadState s m => IndexedSetter i s s a b -> (i -> b) -> m ()
  Set the focus of an optic within a state monad, having access to the index.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(?=) : MonadState s m => Setter s s a (Maybe b) -> b -> m ()
  Set the focus of an optic within a state monad to `Just` a value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(<.=) : MonadState s m => Setter s s a b -> b -> m b
  Set within a state monad with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(<?=) : MonadState s m => Setter s s a (Maybe b) -> b -> m b
  Set to `Just` a value within a state monad with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(+=) : Num a => MonadState s m => Setter' s a -> a -> m ()
  Add a constant value to the focus of an optic within a state monad.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(*=) : Num a => MonadState s m => Setter' s a -> a -> m ()
  Multiply the focus of an optic into state by a constant value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(-=) : Neg a => MonadState s m => Setter' s a -> a -> m ()
  Subtract a constant value from the focus of an optic within a state monad.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(//=) : Fractional a => MonadState s m => Setter' s a -> a -> m ()
  Divide the focus of an optic into state by a constant value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(||=) : MonadState s m => Setter' s Bool -> Lazy Bool -> m ()
  Logically OR the focus of an optic into state with a constant value.

Like `(||)`, this operator takes a lazy second argument.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(&&=) : MonadState s m => Setter' s Bool -> Lazy Bool -> m ()
  Logically AND the focus of an optic into state with a constant value.

Like `(&&)`, this operator takes a lazy second argument.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(<+>=) : Semigroup a => MonadState s m => Setter' s a -> a -> m ()
  Modify the focus of an optic into state using the semigroup/monoid operator.

The constant value is applied to the focus from the right.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4
(<~) : MonadState s m => Setter s s a b -> m b -> m ()
  Run a monadic action and set the focus of an optic in state to the result.

This can be thought of as a variation on the do-notation pseudo-operator (<-),
storing the result of a computation within state instead of in a local
variable.

Totality: total
Visibility: public export
Fixity Declarations:
infix operator, level 1
infixl operator, level 0
(<<~) : MonadState s m => Setter s s a b -> m b -> m b
  Run a monadic action and set the focus of an optic in state to the result.
This is different from `(<~)` in that it also passes though the output of
the action.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 1