Comment by tromp
1 year ago
> you technically can't do name = term
But you can do
let name = term in term2
by de-sugaring it to
((λname. term2) term)
1 year ago
> you technically can't do name = term
But you can do
let name = term in term2
by de-sugaring it to
((λname. term2) term)
This is not relevant since this de-sugaring cannot be performed if `name` is recursive (i.e., if `term` refers to `name`), which `Y` is. So the author's derivation is still required in the pure lambda calculus.