
  0 | module Data.Either.Lens
  1 | 
  2 | import Data.Profunctor
  3 | import public Control.Lens
  4 | 
  5 | %default total
  6 | 
  7 | 
  8 | ||| A prism to the left of an `Either`.
  9 | public export
 10 | Left_ : Prism (Either a c) (Either b c) a b
 11 | Left_ @{MkIsPrism _} = left
 12 | 
 13 | ||| A prism to the right of an `Either`.
 14 | public export
 15 | Right_ : Prism (Either c a) (Either c b) a b
 16 | Right_ @{MkIsPrism _} = right
 17 | 
 18 | 
 19 | public export
 20 | chosen : IndexedLens (Either () ()) (Either a a) (Either b b) a b
 21 | chosen = ilens
 22 |   (either (Left (),) (Right (),))
 23 |   (\case
 24 |     Left _ => Left
 25 |     Right _ => Right)
 26 |