0 | module Data.Tuple.Lens
 1 |
 2 | import Data.Vect
 3 | import Data.Profunctor
 4 | import public Control.Lens
 5 |
 6 | %default total
 7 |
 8 |
 9 | ||| A lens to the first element of a pair.
10 | public export
11 | fst_ : Lens (a, c) (b, c) a b
12 | fst_ @{MkIsLens _} = first
13 |
14 | ||| A lens to the second element of a pair.
15 | public export
16 | snd_ : Lens (c, a) (c, b) a b
17 | snd_ @{MkIsLens _} = second
18 |
19 |
20 | ||| An indexed lens to the first element of a pair, indexed by the other element.
21 | public export
22 | ifst_ : IndexedLens i (a, i) (b, i) a b
23 | ifst_ = ilens swap (flip $ mapFst . const)
24 |
25 | ||| An indexed lens to the second element of a pair, indexed by the other element.
26 | public export
27 | isnd_ : IndexedLens i (i, a) (i, b) a b
28 | isnd_ = ilens id (flip $ mapSnd . const)
29 |