• + 1 comment

    The solution seems to be missing some corner cases where eta-reduction could be applied. For example, test ouput02.txt, line 65, characters 71-75, we have : (BII). It seems to me that it would only happen if we tried to eliminate abstractions from the term (\x. (\y. y) x) where we missed the eta-reduction. My previous solution had (I) instead of (BII), which is equivalent and is what we would expect the elimination to be on the given term. I admit that I don't fully understand why this is happening.