Control.Lens.At

Definitions

interface Ixed : Type -> Type -> Type -> Type

  An interface that provides an `Optional` to access a given index in a
  container, such as an ordinal position in a `List` or `Vect` or a key in a
  map.

Parameters: i, v, a
Methods:

ix : i -> Optional' a v

  An optional that possibly accesses a value at a given index of a container.

Implementations:

Ixed' i i' v a -> Ixed i v a

At i v a -> Ixed i v a

ix : Ixed i v a => i -> Optional' a v

  An optional that possibly accesses a value at a given index of a container.

Totality: total
Visibility: public export

iix : Ixed i v a => i -> IndexedOptional' i a v

  An indexed version of `ix`.

Totality: total
Visibility: public export

interface Ixed' : Type -> Type -> Type -> Type -> Type

  An interface that provides a lens to access a given index in a collection.
  This is different from `Ixed` in that the lens cannot fail to get a value.
  
  Implementations of this interface may use different index types for `ix` and
  `ix'`; for example, `Vect n a` uses `Nat` for `ix` and `Fin n` for `ix'`.

Parameters: i, i', v, a
Constraints: Ixed i v a
Methods:

ix' : i' -> Lens' a v

  A lens that infallibly accesses a value at a given index of a container.

ix' : Ixed' i i' v a => i' -> Lens' a v

  A lens that infallibly accesses a value at a given index of a container.

Totality: total
Visibility: public export

iix' : Ixed' i i' v a => i' -> IndexedLens' i' a v

  An indexed version of `ix'`.

Totality: total
Visibility: public export

interface At : Type -> Type -> Type -> Type

  This interface provides a lens to read, write, add or delete the value
  associated to a key in a map or map-like container.
  
  This lens should satisfy:
  * `ix i == at i . Just_`
  
  If you do not need to add or delete keys, `ix` is more convenient.

Parameters: i, v, a
Constraints: Ixed i v a
Methods:

at : i -> Lens' a (Maybe v)

  A lens that can be used to read, write, add or delete a value associated
  with a key in a map-like container.
  
  If you do not need to add or delete keys, `ix` is more convenient.

at : At i v a => i -> Lens' a (Maybe v)

  A lens that can be used to read, write, add or delete a value associated
  with a key in a map-like container.
  
  If you do not need to add or delete keys, `ix` is more convenient.

Totality: total
Visibility: public export

iat : At i v a => i -> IndexedLens' i a (Maybe v)

  An indexed version of `at`.

Totality: total
Visibility: public export

sans : At i v a => i -> a -> a

  Delete the value at a particular key in a container using `At`.

Totality: total
Visibility: public export

add : At i v a => i -> v -> a -> a

  Add a value at a particular key in a container using `At`.

Totality: total
Visibility: public export