Data.Container.Base.InstanceInterfaces

Definitions

algebraFinite : (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

Visibility: public export

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

Visibility: public export

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

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