Idris2Doc : Control.Lens.Optional

Control.Lens.Optional

(source)
Definitions
record IsOptional : (Type -> Type -> Type) -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkIsOptional : (Strong p, Choice p) -> IsOptional p

  Projection: 
.runIsOptional : IsOptional p -> (Strong p, Choice p)

  Hints:
  
IsOptional p => IsLens p
  
IsOptFold p => IsOptional p
  
IsOptional p => IsOptional (Indexed i p)
  
IsTraversal p => IsOptional p
  
IsOptional p => IsPrism p
.runIsOptional : IsOptional p -> (Strong p, Choice p)
  Totality: total
  Visibility: public export
runIsOptional : IsOptional p -> (Strong p, Choice p)
  Totality: total
  Visibility: public export
optionalToLens : IsOptional p => IsLens p
  Totality: total
  Visibility: export
optionalToPrism : IsOptional p => IsPrism p
  Totality: total
  Visibility: export
indexedOptional : IsOptional p => IsOptional (Indexed i p)
  Totality: total
  Visibility: export
0 Optional : Type -> Type -> Type -> Type -> Type
  An `Optional` is a lens that may or may not contain the focus value.
  As such, accesses will return a `Maybe` value.

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

  Totality: total
  Visibility: public export
0 IndexedOptional : Type -> Type -> Type -> Type -> Type -> Type
  An `IndexedOptional` allows access to the index of a focus.

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

  Totality: total
  Visibility: public export
optional : (s -> Either t a) -> (s -> b -> t) -> Optional s t a b
  Construct an optional from a projection and a setter function.

  Totality: total
  Visibility: public export
optional' : (s -> Maybe a) -> (s -> b -> s) -> Optional s s a b
  Construct a simple optional from a projection and a setter function.

  Totality: total
  Visibility: public export
ioptional : (s -> Either t (i, a)) -> (s -> b -> t) -> IndexedOptional i s t a b
  Construct an indexed optional from a projection and a setter function.

  Totality: total
  Visibility: public export
ioptional' : (s -> Maybe (i, a)) -> (s -> b -> s) -> IndexedOptional i s s a b
  Construct a simple indexed optional from a projection and a setter function.

  Totality: total
  Visibility: public export
ignored : IndexedOptional i s s a b
  The trivial optic that has no focuses.

  Totality: total
  Visibility: public export
filtered : (a -> Bool) -> Optional' a a
  Construct an `Optional` that can be used to filter the focuses of another
  optic.
  
  To be more specific, this optic passes the value through unchanged if it
  satisfies the predicate and returns no values if it does not.
  
  WARNING: This `Optional` is technically invalid! Its setting capability
  should only be used in cases where the focuses that pass the filter aren't
  changed.

  Totality: total
  Visibility: public export
getOptional : Optional s t a b -> (s -> Either t a, s -> b -> t)
  Extract projection and setter functions from an optional.

  Totality: total
  Visibility: public export
withOptional : Optional s t a b -> ((s -> Either t a) -> (s -> b -> t) -> r) -> r
  Extract projection and setter functions from an optional.

  Totality: total
  Visibility: public export
matching : Optional s t a b -> s -> Either t a
  Retrieve the focus value of an optional, or allow its type to change if there
  is no focus.

  Totality: total
  Visibility: public export