git.iko.soy/Idris-dev
on master help sign in
Merge pull request #926 from JanBessai/FunctionTarget
b9b7bbaEdwin Brady
libs/base/Data/Fun.idr+4
compare with master
unifiedsplit
@@ -6,3 +6,7 @@ module Data.Fun
6Fun : Vect n Type -> Type -> Type
6Fun : Vect n Type -> Type -> Type
7Fun [] r = r
7Fun [] r = r
8Fun (t::ts) r = t -> Fun ts r
8Fun (t::ts) r = t -> Fun ts r
9+
10+target : {ts : Vect n Type} -> Fun ts r -> Type
11+target {r} _ = r
12+