Chain higher order Fun types
commit49506602ecacbc9a5a0a5c94109871a8f7d44837
authorJan Bessai <Jan.Bessai@tu-dortmund.de>
dateMon 24 Feb 2014, 11:48 (13 years ago)
parent151d4ef
libs/base/Data/Fun.idr+7
@@ -1,8 +1,15 @@
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--------------------------------------------------------------------------------
68Fun : Vect n Type -> Type -> Type
79Fun [] r = r
810Fun (t::ts) r = t -> Fun ts r
11+
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+