Data.Container.Base.Properties.Instances

Definitions

lambdaNap : IsConcrete (Nap s)

  This is a concrete instance for Naperian containers
  It applies also to `s=Fin n` which is covered by Vect
  We therefore want this to only be applied if Vect isn't

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

(>##) : Vect n a -> Vect' n a

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 0

(##>) : Vect' n a -> Vect n a

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 0

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

foldList : (a -> b -> b) -> b -> List' a -> b

Totality: total
Visibility: public export