Online TDPE (2)
Extend any value destructors to treat residual code [Sumii & Kobayashi 99]
tl' x = tl x¡¡(if x is a list)
tl' x = tl x¡¡(if x is residual code)
For example:
?int_list?int_list (?a. (tl' (tl' (3 :: a)))= ?x. (?a. (tl' (tl' (3 :: a))) @ x= ?x. tl' (tl' (3 :: x))= ?x. tl' x= ?x. tl x