interface Indexable : Type -> (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type- Parameters: i, p, p'
Methods:
indexed : p' a b -> p (i, a) b
Implementation: IsIso p => Indexable i p p
indexed : Indexable i p p' => p' a b -> p (i, a) b- Totality: total
Visibility: public export 0 IndexedOptic' : (Type -> Type -> Type) -> Type -> Type -> Type -> Type -> Type -> Type- Totality: total
Visibility: public export 0 IndexedOptic : ((Type -> Type -> Type) -> Type) -> Type -> Type -> Type -> Type -> Type -> Type- Totality: total
Visibility: public export record Indexed : Type -> (Type -> Type -> Type) -> Type -> Type -> Type- Totality: total
Visibility: public export
Constructor: MkIndexed : p (i, a) b -> Indexed i p a b
Projection: .runIndexed : Indexed i p a b -> p (i, a) b
Hints:
Bicontravariant p => Bicontravariant (Indexed i p)Bifunctor p => Bifunctor (Indexed i p)Closed p => Closed (Indexed i p)Bifunctor ten => GenStrong ten p => GenStrong ten (Indexed i p)IsGetter p => IsGetter (Indexed i p)IsIso p => IsIso (Indexed i p)IsLens p => IsLens (Indexed i p)IsOptFold p => IsOptFold (Indexed i p)IsOptional p => IsOptional (Indexed i p)IsPrism p => IsPrism (Indexed i p)IsSetter p => IsSetter (Indexed i p)IsTraversal p => IsTraversal (Indexed i p)Mapping p => Mapping (Indexed i p)Profunctor p => Profunctor (Indexed i p)Traversing p => Traversing (Indexed i p)
.runIndexed : Indexed i p a b -> p (i, a) b- Totality: total
Visibility: public export runIndexed : Indexed i p a b -> p (i, a) b- Totality: total
Visibility: public export indexedIso : IsIso p => IsIso (Indexed i p)- Totality: total
Visibility: export icompose : IsIso p => (i -> j -> k) -> IndexedOptic' p i s t a b -> IndexedOptic' (Indexed i p) j a b a' b' -> IndexedOptic' p k s t a' b' Compose two indexed optics, using a function to combine the indices of each
optic.
Totality: total
Visibility: public export(<.>) : IsIso p => IndexedOptic' p i s t a b -> IndexedOptic' (Indexed i p) j a b a' b' -> IndexedOptic' p (i, j) s t a' b' Compose two indexed optics, returning an optic indexed by a pair of indices.
Mnemonically, the angle brackets point to the fact that we want to preserve
both indices.
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9(.>) : Optic' p s t a b -> IndexedOptic' p i a b a' b' -> IndexedOptic' p i s t a' b' Compose a non-indexed optic with an indexed optic.
Mnemonically, the angle bracket points to the index that we want to preserve.
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9(<.) : IndexedOptic' p i s t a b -> Optic' (Indexed i p) a b a' b' -> IndexedOptic' p i s t a' b' Compose an indexed optic with a non-indexed optic.
Mnemonically, the angle bracket points to the index that we want to preserve.
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9constIndex : IsIso p => i -> Optic' p s t a b -> IndexedOptic' p i s t a b Augment an optic with an index that is constant for all inputs.
Totality: total
Visibility: public exportreindexed : IsIso p => (i -> j) -> IndexedOptic' p i s t a b -> IndexedOptic' p j s t a b Modify the indices of an indexed optic.
Totality: total
Visibility: public export