Idris2Doc : Control.Lens.Iso

Control.Lens.Iso

(source)
Definitions
record IsIso : (Type -> Type -> Type) -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkIsIso : Profunctor p -> IsIso p

  Projection: 
.runIsIso : IsIso p -> Profunctor p

  Hints:
  
IsIso p => Indexable i p p
  
IsLens p => IsIso p
  
IsIso p => IsIso (Indexed i p)
  
IsPrism p => IsIso p
.runIsIso : IsIso p -> Profunctor p
  Totality: total
  Visibility: public export
runIsIso : IsIso p -> Profunctor p
  Totality: total
  Visibility: public export
0 Iso : Type -> Type -> Type -> Type -> Type
  An `Iso` is an isomorphism family between types. It allows a value to be
  converted or updated across this isomorphism.

  Totality: total
  Visibility: public export
0 Iso' : Type -> Type -> Type
  An `Iso'` is an isomorphism family between types. It allows a value to be
  converted or updated across this isomorphism.
  This is the `Simple` version of `Iso`.

  Totality: total
  Visibility: public export
getIso : Iso s t a b -> (s -> a, b -> t)
  Extract the conversion functions from an `Iso`.

  Totality: total
  Visibility: public export
withIso : Iso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
  Extract the conversion functions from an `Iso`.

  Totality: total
  Visibility: public export
iso : (s -> a) -> (b -> t) -> Iso s t a b
  Construct an `Iso` from two inverse functions.

  Totality: total
  Visibility: public export
fromEqv : s <=> a -> Iso' s a
  Construct a simple `Iso` from an equivalence.

  Totality: total
  Visibility: public export
from : Iso s t a b -> Iso b a t s
  Invert an isomorphism.

  Totality: total
  Visibility: public export
au : Functor f => Iso s t a b -> ((b -> t) -> f s) -> f a
  Based on Epigram's `ala`.

  Totality: total
  Visibility: public export
auf : (Functor f, Functor g) => Iso s t a b -> (f t -> g s) -> f b -> g a
  Based on Epigram's `ala'`.

  Totality: total
  Visibility: public export
xplat : Functor f => Iso s t a b -> ((s -> a) -> f b) -> f t
  An alias for `au . from`.

  Totality: total
  Visibility: public export
xplatf : (Functor f, Functor g) => Iso s t a b -> (f a -> g b) -> f s -> g t
  an alias for `auf . from`.

  Totality: total
  Visibility: public export
under : Iso s t a b -> (t -> s) -> b -> a
  Update a value under an `Iso`, as opposed to `over` it.
  In other words, this is a convenient alias for `over . from`.

  Totality: total
  Visibility: public export
constant : a -> Iso (a -> b) (a' -> b') b b'
  An "isomorphism" between a function and its result type, assuming that
  the parameter type is inhabited.

  Totality: total
  Visibility: public export
involuted : (a -> a) -> Iso' a a
  Construct an isomorphism given an involution.

  Totality: total
  Visibility: public export
flipped : Iso (a -> b -> c) (a' -> b' -> c') (b -> a -> c) (b' -> a' -> c')
  Flipping a function's arguments forms an isomorphism.

  Totality: total
  Visibility: public export
swapped : Symmetric f => Iso (f a b) (f a' b') (f b a) (f b' a')
  Swapping a symmetric tensor product's parameters is an isomorphism.

  Totality: total
  Visibility: public export
casted : (Cast s a, Cast b t) => Iso s t a b
  Casting between types forms an isomorphism.
  WARNING: This is only a true isomorphism if casts in both directions are
  lossless and mutually inverse.

  Totality: total
  Visibility: public export
non : Eq a => a -> Iso' (Maybe a) a
  The isomorphism `non x` converts between `Maybe a` and `a` sans the
  element `x`.
  
  This is useful for working with optics whose focus type is `Maybe a`,
  such as `at`.

  Totality: total
  Visibility: public export
Id_ : Iso (Identity a) (Identity b) a b
  Totality: total
  Visibility: public export
Const_ : Iso (Const a b) (Const c d) a c
  Totality: total
  Visibility: public export
mapping : (Functor f, Functor g) => Iso s t a b -> Iso (f s) (g t) (f a) (g b)
  Lift an isomorphism through a `Functor`.

  Totality: total
  Visibility: public export
contramapping : (Contravariant f, Contravariant g) => Iso s t a b -> Iso (f a) (g b) (f s) (g t)
  Lift an isomorphism through a `Contravariant` functor.

  Totality: total
  Visibility: public export
bimapping : (Bifunctor f, Bifunctor g) => Iso s t a b -> Iso s' t' a' b' -> Iso (f s s') (g t t') (f a a') (g b b')
  Lift isomorphisms through a `Bifunctor`.

  Totality: total
  Visibility: public export
mappingFst : (Bifunctor f, Bifunctor g) => Iso s t a b -> Iso (f s x) (g t y) (f a x) (g b y)
  Lift an isomorphism through the first parameter of a `Bifunctor`.

  Totality: total
  Visibility: public export
mappingSnd : (Bifunctor f, Bifunctor g) => Iso s t a b -> Iso (f x s) (g y t) (f x a) (g y b)
  Lift an isomorphism through the second parameter of a `Bifunctor`.

  Totality: total
  Visibility: public export
dimapping : (Profunctor f, Profunctor g) => Iso s t a b -> Iso s' t' a' b' -> Iso (f a s') (g b t') (f s a') (g t b')
  Lift isomorphisms through a `Profunctor`.

  Totality: total
  Visibility: public export
lmapping : (Profunctor f, Profunctor g) => Iso s t a b -> Iso (f a x) (g b y) (f s x) (g t y)
  Lift an isomorphism through the first parameter of a `Profunctor`.

  Totality: total
  Visibility: public export
rmapping : (Profunctor f, Profunctor g) => Iso s t a b -> Iso (f x s) (g y t) (f x a) (g y b)
  Lift an isomorphism through the second parameter of a `Profunctor`.

  Totality: total
  Visibility: public export