- absts (C.Appl (S.lift n t :: args))
-
-let get_tys c decurry t =
- let tys, _ = split c (get_type c t) in
- let tys, _ = HEL.split_nth decurry (List.tl tys) in
- List.rev tys
+ let t = match S.lift n t with
+ | C.Appl ts -> C.Appl (ts @ args)
+ | t -> C.Appl (t :: args)
+ in
+ g (absts t)
+
+let get_tys c decurry =
+ let rec aux n = function
+(* | C.Appl (hd :: tl) -> aux (n + List.length tl) hd *)
+ | t ->
+ let tys, _ = split c (get_type c t) in
+ let _, tys = HEL.split_nth n (List.rev tys) in
+ let tys, _ = HEL.split_nth decurry tys in
+ tys
+ in
+ aux 0