git.iko.soy/Idris-dev
on 0875310 help sign in
Idris-dev/libs/base/Data/Fun.idr
12 lines 395 B history raw
1module Data.Fun
3--------------------------------------------------------------------------------
4-- Build an n-ary function type from a Vect of Types and a result type
5--------------------------------------------------------------------------------
6Fun : Vect n Type -> Type -> Type
7Fun [] r = r
8Fun (t::ts) r = t -> Fun ts r
10target : {ts : Vect n Type} -> Fun ts r -> Type
11target {r} _ = r