@@ -1,5 +1,7 @@
11module Data.Fun
22
3+%default total
4+
35--------------------------------------------------------------------------------
46-- Build an n-ary function type from a Vect of Types and a result type
57--------------------------------------------------------------------------------
@@ -7,6 +9,10 @@ Fun : Vect n Type -> Type -> Type
79Fun [] r = r
810Fun (t::ts) r = t -> Fun ts r
911
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)
15+
1016target : {ts : Vect n Type} -> Fun ts r -> Type
1117target {r} _ = r
1218