Idris2Doc : Data.Fun

Data.Fun

Reexports
import public Data.Vect
Definitions
Fun : Vect n Type -> Type -> Type
  Build an n-ary function type from a Vect of Types and a result type

  Totality: total
  Visibility: public export
chain : Fun [r] r' -> Fun ts r -> Fun ts r'
  Totality: total
  Visibility: public export
target : Fun ts r -> Type
  Returns the co-domain of a n-ary function.

  Totality: total
  Visibility: public export