Data.Container.Base.Extension.Instances

Definitions

Scalar' : Type -> Type

  Isomorphic to the Identity

Visibility: public export

Pair' : Type -> Type

  Isomorphic to Pair

Visibility: public export

Either' : Type -> Type

  Isomorphic to Either

Visibility: public export

Maybe' : Type -> Type

  Isomorphic to Maybe

Visibility: public export

List' : Type -> Type

  Isomorphic to List

Visibility: public export

Vect' : Nat -> Type -> Type

  Isomorphic to Vect

Visibility: public export

Stream' : Type -> Type

  Isomorphic to Stream

Visibility: public export

BinTree' : Type -> Type

  Isomorphic to Data.Tree.BinTreeSame

Visibility: public export

BinTreeNode' : Type -> Type

  Isomorphic to Data.Tree.BinTreeNode

Visibility: public export

BinTreeLeaf' : Type -> Type

  Isomorphic to Data.Tree.BinTreeLeaf

Visibility: public export

composeExtensions : List Cont -> Type -> Type

Visibility: public export

composeExtensions : Vect n Cont -> Type -> Type

Visibility: public export

EmptyExt : IsNaperian c => Ext c ()

Visibility: public export

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

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

Visibility: public export