@@ -1,5 +1,7 @@
1module Data.Fun
1module Data.Fun
3--------------------------------------------------------------------------------
5--------------------------------------------------------------------------------
4-- Build an n-ary function type from a Vect of Types and a result type
6-- Build an n-ary function type from a Vect of Types and a result type
5--------------------------------------------------------------------------------
7--------------------------------------------------------------------------------
@@ -7,6 +9,10 @@ Fun : Vect n Type -> Type -> Type
7Fun [] r = r
9Fun [] r = r
8Fun (t::ts) r = t -> Fun ts r
10Fun (t::ts) r = t -> Fun ts r
12+chain : {ts : Vect n Type} -> Fun [r] r' -> Fun ts r -> Fun ts r'
13+chain {ts = []} g r = g r
14+chain {ts = (_::_)} g f = \ x => chain g (f x)
10target : {ts : Vect n Type} -> Fun ts r -> Type
16target : {ts : Vect n Type} -> Fun ts r -> Type
11target {r} _ = r
17target {r} _ = r