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'