Data.Container.Base.Extension.Instances

Definitions

Scalar' : Type -> Type

  Isomorphic to the Identity

Totality: total
Visibility: public export

Pair' : Type -> Type

  Isomorphic to Pair

Totality: total
Visibility: public export

Either' : Type -> Type

  Isomorphic to Either

Totality: total
Visibility: public export

Maybe' : Type -> Type

  Isomorphic to Maybe

Totality: total
Visibility: public export

List' : Type -> Type

  Isomorphic to List

Totality: total
Visibility: public export

Vect' : Nat -> Type -> Type

  Isomorphic to Vect

Totality: total
Visibility: public export

Stream' : Type -> Type

  Isomorphic to Stream

Totality: total
Visibility: public export

BinTree' : Type -> Type

  Isomorphic to Data.Tree.BinTreeSame

Totality: total
Visibility: public export

BinTreeNode' : Type -> Type

  Isomorphic to Data.Tree.BinTreeNode

Totality: total
Visibility: public export

BinTreeLeaf' : Type -> Type

  Isomorphic to Data.Tree.BinTreeLeaf

Totality: total
Visibility: public export

composeExtensions : List Cont -> Type -> Type

Totality: total
Visibility: public export

composeExtensions : Vect n Cont -> Type -> Type

Totality: total
Visibility: public export

EmptyExt : IsNaperian c => Ext c ()

Totality: total
Visibility: public export

liftA2ConstCont : IsNaperian c => Ext c a -> Ext c b -> Ext c (a, b)

Totality: total
Visibility: public export

positionsCont : Ext c (c .Pos sh)

  Generalisation of 'positions' from Data.Functor.Naperian
  Works for an arbitrary container, as long as we supply its shape
  The definition in Data.Functor.Naperian.positions is for Naperian containers
  i.e. containers with a unit shape

Totality: total
Visibility: public export

set : InterfaceOnPositions c Eq => (e : Ext c x) -> c .Pos (shapeExt e) -> x -> Ext c x

  The `index` field of an extension defines a "getter" for a container
  This is the container setter

Totality: total
Visibility: public export