Idris2Doc : Data.Telescope.Fun

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.

Fun : (env : Environment gamma) -> (0 delta : Segment n gamma) -> SimpleFun env delta Type -> Type
curry : ((ext : Environment env delta) -> uncurry cod ext) -> Fun env delta cod
uncurry : Fun env delta cod -> (ext : Environment env delta) -> uncurry cod ext