Name collisions not handled in β-reduction

[Yan-1999]

The term (λx. λy. x y) y should be reduced to λz. y z instead of λy. y y to avoid name collisions.

[asukaminato0721]

My implement gives

Result of complex example: \y1. y y1

lol.

https://github.com/asukaminato0721/cs242/blob/master/lambda/src/main.rs#L280

[sshwy]

Actually this collision is just a visual misdirection. The implentation use De Bruijn index to represent variables so further reduction is still correct: