Idris2Doc : Data.Either.Lens

Data.Either.Lens

(source)
Reexports
import public Control.Lens
Definitions
Left_ : Prism (Either a c) (Either b c) a b
  A prism to the left of an `Either`.

  Totality: total
  Visibility: public export
Right_ : Prism (Either c a) (Either c b) a b
  A prism to the right of an `Either`.

  Totality: total
  Visibility: public export
chosen : IndexedLens (Either () ()) (Either a a) (Either b b) a b
  Totality: total
  Visibility: public export