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

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

algebraFinite : (0 c : Cont) -> IsFinite c => (0 a : Type) -> Num a => Algebra (Ext c) a

  Any finite container (i.e. whose each set of positions is finite) can be
  given an algebra instance simply by summing up all the concrete values

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 Declarations:
infixr operator, level 7
infixr operator, level 7