- let var = head_of_inert p.div in\r
- print_cmd "STEP" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
- let rec aux' p m t =\r
- if m < 0\r
- then p, t\r
- else\r
- let p, v = freshvar p in\r
- let p, t = aux' p (m-1) t in\r
- p, A(t, V (v + k + 1)) in\r
- let p, t = aux' p n (V 0) in\r
- let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V (k-m)) in\r
- let rec aux m t =\r
- if m < 0\r
- then aux' (k-1) t\r
- else L (aux (m-1) t) in\r
- let t = aux k t in\r
+ let var, _ = get_inert p.div in\r
+print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
+ let p, t = (* apply fresh vars *)\r
+ fold_nat (fun (p, t) _ ->\r
+ let p, v = freshvar p in\r
+ p, A(t, V (v + k + 1))\r
+ ) (p, V 0) n in\r
+ let t = (* apply unused bound variables V_{k-1}..V_1 *)\r
+ fold_nat (fun t m -> A(t, V (k-m+1))) t k in\r
+ let t = mk_lams t (k+1) in (* make leading lambdas *)\r