shortcut to obtain the target type of a function
commitb6dab40666069a48d38afa73fb9edbc27a03be8c
authorJan Bessai <Jan.Bessai@tu-dortmund.de>
dateMon 24 Feb 2014, 08:50 (13 years ago)
parent151d4ef
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+