Merge pull request #926 from JanBessai/FunctionTarget
Shortcut to obtain the target type of a function
commitb9b7bba94d17013207ae68cfb9ad76cd5d05235d
authorEdwin Brady <edwin.brady@gmail.com>
dateTue 25 Feb 2014, 22:55 (13 years ago)
parent3489bf2b6dab40
libs/base/Data/Fun.idr+4
@@ -6,3 +6,7 @@ module Data.Fun
66Fun : Vect n Type -> Type -> Type
77Fun [] r = r
88Fun (t::ts) r = t -> Fun ts r
9+
10+target : {ts : Vect n Type} -> Fun ts r -> Type
11+target {r} _ = r
12+