IdrisDoc: Data.Chain

# Data.Chain

Chain : Nat -> (i : Type) -> (o : Type) -> Type

  Repeated function application

EndoChain : Nat -> Type -> Type

  Repeated endofunction application

after : (o -> o') -> Chain n i o -> Chain n i o'

  (.) generalized to any number of arguments.

before : (i -> i') -> Chain n i' o -> Chain n i o

  `on` generalized to any number of arguments

fromVectFunc : (Vect n i -> o) -> Chain n i o

  Apply a function over a vector to our new type

packVect : Chain n i (Vect n i)

  Create a vect of a given length from the arguments given.

reflexes : Chain n i o -> i -> o

  Fill in the same argument for all items (available for a single argument as
  Data.Combinators.reflex)

withIso : Iso t t' -> EndoChain n t -> EndoChain n t'