Control.Lens.Prism

Definitions

record IsPrism : (Type -> Type -> Type) -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsPrism : Choice p -> IsPrism p

Projection: 

.runIsPrism : IsPrism p -> Choice p

Hints:

IsPrism p => IsIso p

IsReview p => IsPrism p

IsOptional p => IsPrism p

IsPrism p => IsPrism (Indexed i p)

.runIsPrism : IsPrism p -> Choice p

Totality: total
Visibility: public export

runIsPrism : IsPrism p -> Choice p

Totality: total
Visibility: public export

prismToIso : IsPrism p => IsIso p

Totality: total
Visibility: export

indexedPrism : IsPrism p => IsPrism (Indexed i p)

Totality: total
Visibility: export

0 Prism : Type -> Type -> Type -> Type -> Type

  A prism is a first-class reference to one of the cases of a sum type.
  Prisms allow one to determine whether a value matches the focused case
  and extract the corresponding data if it does.
  
  More precisely, a `Prism` is an `Optional` that can be flipped to obtain
  a `Getter` in the opposite direction.

Totality: total
Visibility: public export

0 Prism' : Type -> Type -> Type

  `Prism'` is the `Simple` version of `Prism`.

Totality: total
Visibility: public export

0 IndexedPrism : Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: public export

0 IndexedPrism' : Type -> Type -> Type -> Type

Totality: total
Visibility: public export

prism : (b -> t) -> (s -> Either t a) -> Prism s t a b

  Construct a prism from injection and projection functions.

Totality: total
Visibility: public export

prism' : (b -> s) -> (s -> Maybe a) -> Prism s s a b

  Construct a simple prism from injection and projection functions.

Totality: total
Visibility: public export

iprism : (b -> t) -> (s -> Either t (i, a)) -> IndexedPrism i s t a b

Totality: total
Visibility: public export

iprism' : (b -> s) -> (s -> Maybe (i, a)) -> IndexedPrism i s s a b

Totality: total
Visibility: public export

getPrism : Prism s t a b -> (b -> t, s -> Either t a)

  Extract injection and projection functions from a prism.

Totality: total
Visibility: public export

withPrism : Prism s t a b -> ((b -> t) -> (s -> Either t a) -> r) -> r

  Extract injection and projection functions from a prism.

Totality: total
Visibility: public export

nearly : a -> (a -> Bool) -> Prism' a ()

  Construct a prism that uses a predicate to determine if a value matches.

Totality: total
Visibility: public export

only : Eq a => a -> Prism' a ()

  Construct a prism that matches only one value.

Totality: total
Visibility: public export

without : Prism s t a b -> Prism s' t' a' b' -> Prism (Either s s') (Either t t') (Either a a') (Either b b')

  Create a prism that operates on `Either` values from two other prisms.
  
  This can be seen as dual to `alongside`.

Totality: total
Visibility: public export

below : Traversable f => Prism' s a -> Prism' (f s) (f a)

  Lift a prism through a `Traversable` container.
  
  The constructed prism will only match if all of the inner elements of the
  `Traversable` container match.

Totality: total
Visibility: public export

aside : Prism s t a b -> Prism (e, s) (e, t) (e, a) (e, b)

  Lift a prism through part of a product type.

Totality: total
Visibility: public export