Control.Lens.OptionalFold

Definitions

record IsOptFold : (Type -> Type -> Type) -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsOptFold : (Strong p, (Choice p, Bicontravariant p)) -> IsOptFold p

Projection: 

.runIsOptFold : IsOptFold p -> (Strong p, (Choice p, Bicontravariant p))

Hints:

IsOptFold p => IsGetter p

IsOptFold p => IsOptFold (Indexed i p)

IsFold p => IsOptFold p

IsOptFold p => IsOptional p

.runIsOptFold : IsOptFold p -> (Strong p, (Choice p, Bicontravariant p))

Totality: total
Visibility: public export

runIsOptFold : IsOptFold p -> (Strong p, (Choice p, Bicontravariant p))

Totality: total
Visibility: public export

optFoldToOptional : IsOptFold p => IsOptional p

Totality: total
Visibility: export

optFoldToGetter : IsOptFold p => IsGetter p

Totality: total
Visibility: export

indexedOptFold : IsOptFold p => IsOptFold (Indexed i p)

Totality: total
Visibility: export

0 OptionalFold : Type -> Type -> Type

  An `OptionalFold` is a getter that may not return a focus value.
  `OptionalFold s a` is equivalent to `s -> Maybe a`.

Totality: total
Visibility: public export

0 IndexedOptionalFold : Type -> Type -> Type -> Type

  An `IndexedOptionalFold` returns an index while getting.

Totality: total
Visibility: public export

folding : (s -> Maybe a) -> OptionalFold s a

  Construct an `OptionalFold` from a function.

Totality: total
Visibility: public export

ifolding : (s -> Maybe (i, a)) -> IndexedOptionalFold i s a

  Construct an `IndexedOptionalFold` from a function.

Totality: total
Visibility: public export