\r
let compute_max_lambdas_at hd_var j =\r
let rec aux hd = function\r
- | A(t1,t2) ->\r
+ | A(t1,t2) -> max (max (aux hd t1) (aux hd t2))\r
(if get_inert t1 = (V hd, j)\r
- then max ( (*FIXME*)\r
- if is_inert t2 && let hd', j' = get_inert t2 in hd' = V hd\r
- then let hd', j' = get_inert t2 in j - j'\r
- else no_leading_lambdas hd_var j t2)\r
- else id) (max (aux hd t1) (aux hd t2))\r
+ then no_leading_lambdas hd (j+1) t2\r
+ else 0)\r
| L(t,_) -> aux (hd+1) t\r
- | V _ | C -> 0\r
+ | V _\r
+ | C -> 0\r
in aux hd_var\r
;;\r
\r