Control.Lens.Cons

Definitions

interface Cons : Type -> Type -> Type -> Type -> Type

  An interface that provides a way to detach and inspect elements from the
  left side of a sequence.

Parameters: s, t, a, b
Methods:

consIso : Iso s t (Maybe (a, s)) (Maybe (b, t))

  An isomorphism that can inspect the left side of a sequence.

cons_ : Prism s t (a, s) (b, t)

  A prism that can attach or detach a value from the left side of a
  sequence.

consIso : Cons s t a b => Iso s t (Maybe (a, s)) (Maybe (b, t))

  An isomorphism that can inspect the left side of a sequence.

Totality: total
Visibility: public export

cons_ : Cons s t a b => Prism s t (a, s) (b, t)

  A prism that can attach or detach a value from the left side of a
  sequence.

Totality: total
Visibility: public export

head_ : Cons s s a a => Optional' s a

  Access the head (left-most element) of a sequence, if it is non-empty.

Totality: total
Visibility: public export

tail_ : Cons s s a a => Optional' s s

  Access the tail (all but the left-most element) of a sequence, if it is
  non-empty.

Totality: total
Visibility: public export

nil : Cons s s a a => s

  Use a `Cons` implementation to construct an empty sequence.

Totality: total
Visibility: public export

interface Snoc : Type -> Type -> Type -> Type -> Type

  An interface that provides a way to detach and inspect elements from the
  right side of a sequence.

Parameters: s, t, a, b
Methods:

snocIso : Iso s t (Maybe (s, a)) (Maybe (t, b))

  An isomorphism that can inspect the right side of a sequence.

snoc_ : Prism s t (s, a) (t, b)

  This is a prism that can attach or detach a value from the right side of a
  sequence.

snocIso : Snoc s t a b => Iso s t (Maybe (s, a)) (Maybe (t, b))

  An isomorphism that can inspect the right side of a sequence.

Totality: total
Visibility: public export

snoc_ : Snoc s t a b => Prism s t (s, a) (t, b)

  This is a prism that can attach or detach a value from the right side of a
  sequence.

Totality: total
Visibility: public export

init_ : Snoc s s a a => Optional' s s

  Access all but the right-most element of a sequence, if it is non-empty.

Totality: total
Visibility: public export

last_ : Snoc s s a a => Optional' s a

  Access the last (right-most) element of a sequence, if it is non-empty.

Totality: total
Visibility: public export

lin : Snoc s s a a => s

  Use a `Snoc` implementation to construct an empty sequence.

Totality: total
Visibility: public export