Idris2Doc : Data.Telescope.SimpleFun

Data.Telescope.SimpleFun

SimpleFun : Environmentgamma -> (0 _ : Segmentngamma) -> Type -> Type
An n-ary function whose codomain does not depend on its
arguments. The arguments may have dependencies.
curry : (Environmentenvdelta -> cod) -> SimpleFunenvdeltacod
target : SimpleFunenvdeltacod -> Type
uncurry : SimpleFunenvdeltacod -> Environmentenvdelta -> cod