git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/base/Data/Fun.idr
15 lines 389 B history raw
1module Data.Fun
3%default total
5||| Build an n-ary function type from a Vect of Types and a result type
6Fun : Vect n Type -> Type -> Type
7Fun [] r = r
8Fun (t::ts) r = t -> Fun ts r
10chain : {ts : Vect n Type} -> Fun [r] r' -> Fun ts r -> Fun ts r'
11chain {ts = []} g r = g r
12chain {ts = (_::_)} g f = \ x => chain g (f x)
14target : {ts : Vect n Type} -> Fun ts r -> Type
15target {r} _ = r