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