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.

Definitions

0 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.

Visibility: public export

target : SimpleFun env delta cod -> Type

Visibility: public export

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

Visibility: public export

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

Visibility: public export