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

fixShape : Ext c a -> Cont

Totality: total
Visibility: public export

Pick : Cont -> Type -> Cont

  Continer describing how from an extension of another we can get a value out

Totality: total
Visibility: public export

composeExtensions : Vect n Cont -> Type -> Type

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

fromList : List a -> List' a

Totality: total
Visibility: public export

toList : List' a -> List a

Totality: total
Visibility: public export

fromVect : Vect n a -> Vect' n a

Totality: total
Visibility: public export

toVect : Vect' n a -> Vect n a

Totality: total
Visibility: public export

fromBinTreeSame : BinTreeSame a -> BinTree' a

Totality: total
Visibility: public export

toBinTreeSame : BinTree' a -> BinTreeSame a

Totality: total
Visibility: public export

fromTreeHelper : BinTreePosNode LeafS -> a

Totality: total
Visibility: public export

fromBinTreeNode : BinTreeNode a -> BinTreeNode' a

Totality: total
Visibility: public export

toBinTreeNode : BinTreeNode' a -> BinTreeNode a

Totality: total
Visibility: public export

fromBinTreeLeaf : BinTreeLeaf a -> BinTreeLeaf' a

Totality: total
Visibility: public export

toBinTreeLeaf : BinTreeLeaf' a -> BinTreeLeaf a

Totality: total
Visibility: public export

take : (s : Fin (S n)) -> Vect' n a -> Vect' (finToNat s) a

Totality: total
Visibility: public export

(++) : Vect' n a -> Vect' m a -> Vect' (n + m) a

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7