git.iko.soy/Idris-dev
on master help sign in
Chain higher order Fun types
4950660Jan Bessai
libs/base/Data/Fun.idr+7
compare with master
unifiedsplit
@@ -1,8 +1,15 @@
1module Data.Fun
1module Data.Fun
2
2
3+%default total
4+
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--------------------------------------------------------------------------------
6Fun : Vect n Type -> Type -> Type
8Fun : 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
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+