Data.Telescope.Fun

N-ary dependent functions using telescopes

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

Definitions

0 Fun : (env : Environment gamma) -> (0 delta : Segment n gamma) -> SimpleFun env delta Type -> Type

Visibility: public export

uncurry : Fun env delta cod -> (ext : Environment env delta) -> uncurry cod ext

Visibility: public export

curry : ((ext : Environment env delta) -> uncurry cod ext) -> Fun env delta cod

Visibility: public export