Idris2Doc : Data.Maybe.Lens

Data.Maybe.Lens

(source)
Reexports
import public Control.Lens
Definitions
Nothing_ : Prism (Maybe a) (Maybe b) () ()
  A prism of the `Nothing` case of a `Maybe`.

  Totality: total
  Visibility: public export
Just_ : Prism (Maybe a) (Maybe b) a b
  A prism of the `Just` case of a `Maybe`.

  Totality: total
  Visibility: public export
(.?) : IsPrism p => Optic' p s t (Maybe a) (Maybe b) -> Optic' p a b a' b' -> Optic' p s t a' b'
  The composition `l .? l'` is equivalent to `l . Just_ . l'`.
  Useful for optics whose focus type is a `Maybe`, such as `at`.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 9