Control.Lens.Getter

Definitions

record IsGetter : (Type -> Type -> Type) -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsGetter : (Strong p, Bicontravariant p) -> IsGetter p

Projection: 

.runIsGetter : IsGetter p -> (Strong p, Bicontravariant p)

Hints:

IsOptFold p => IsGetter p

IsGetter p => IsGetter (Indexed i p)

IsGetter p => IsLens p

.runIsGetter : IsGetter p -> (Strong p, Bicontravariant p)

Totality: total
Visibility: public export

runIsGetter : IsGetter p -> (Strong p, Bicontravariant p)

Totality: total
Visibility: public export

getterToLens : IsGetter p => IsLens p

Totality: total
Visibility: export

indexedGetter : IsGetter p => IsGetter (Indexed i p)

Totality: total
Visibility: export

0 Getter : Type -> Type -> Type

  A getter is an optic that only supports getting, not setting.
  
  `Getter s a` is equivalent to a simple function `s -> a`.

Totality: total
Visibility: public export

0 IndexedGetter : Type -> Type -> Type -> Type

  An indexed getter returns an index while getting.

Totality: total
Visibility: public export

to : (s -> a) -> Getter s a

  Construct a getter from a function.

Totality: total
Visibility: public export

ito : (s -> (i, a)) -> IndexedGetter i s a

  Construct an indexed getter from a function.

Totality: total
Visibility: public export

like : a -> Getter s a

  Construct a getter that always returns a constant value.

Totality: total
Visibility: public export

views : Getter s a -> (a -> r) -> s -> r

  Access the value of an optic and apply a function to it, returning the result.

Totality: total
Visibility: public export

view : Getter s a -> s -> a

  Access the focus value of an optic, particularly a `Getter`.

Totality: total
Visibility: public export

iviews : IndexedGetter i s a -> (i -> a -> r) -> s -> r

  Access the value and index of an optic and apply a function to them,
  returning the result.

Totality: total
Visibility: public export

iview : IndexedGetter i s a -> s -> (i, a)

  Access the focus value and index of an optic, particularly a `Getter`.

Totality: total
Visibility: public export

(^.) : s -> Getter s a -> a

  Access the focus value of an optic, particularly a `Getter`.
  
  This is the operator form of `view`.

Totality: total
Visibility: public export
Fixity Declarations:
infixl operator, level 8
infixl operator, level 8

(^@.) : s -> IndexedGetter i s a -> (i, a)

  Access the focus value and index of an optic, particularly a `Getter`.
  
  This is the operator form of `iview`.

Totality: total
Visibility: public export
Fixity Declarations:
infixl operator, level 8
infixl operator, level 8