Idris2Doc : Data.Tuple.Lens

Data.Tuple.Lens

(source)
Reexports
import public Control.Lens
Definitions
fst_ : Lens (a, c) (b, c) a b
  A lens to the first element of a pair.

  Totality: total
  Visibility: public export
snd_ : Lens (c, a) (c, b) a b
  A lens to the second element of a pair.

  Totality: total
  Visibility: public export
ifst_ : IndexedLens i (a, i) (b, i) a b
  An indexed lens to the first element of a pair, indexed by the other element.

  Totality: total
  Visibility: public export
isnd_ : IndexedLens i (i, a) (i, b) a b
  An indexed lens to the second element of a pair, indexed by the other element.

  Totality: total
  Visibility: public export