git.iko.soy/Idris-dev
on ec2a48a help sign in
Idris-dev/libs/base/Data/Fun.idr
17 lines 407 B history raw
1module Data.Fun
3import Data.Vect
5%default total
7||| Build an n-ary function type from a Vect of Types and a result type
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