Idris2Doc : Data.Telescope.SimpleFun

Data.Telescope.SimpleFun

N-ary simple (non-dependent) functions using telescopes

Compare with `base/Data.Fun` and `contrib/Data.Fun.Extra` and with:
Guillaume Allais. 2019. Generic level polymorphic n-ary functions. TyDe 2019.

SimpleFun : Environment gamma -> (0 _ : Segment n gamma) -> Type -> Type

  An n-ary function whose codomain does not depend on its
  arguments. The arguments may have dependencies.

curry : (Environment env delta -> cod) -> SimpleFun env delta cod

target : SimpleFun env delta cod -> Type

uncurry : SimpleFun env delta cod -> Environment env delta -> cod