pi8027/typeinfer — Issue #37: p6 EQ-ABSについての質問
Author: cutsea110
Created: 2011-11-13 22:56:03+00:00
State: open

e =α e' の時、λx.e =α λx.e' なんですが、
eが仮にy+1という式だったとした場合、e'=x+1はα同値ですよね？
その場合、λx.e =α λx.e'は λx.y+1 =α λx.x+1となってしまってα同値じゃない気がしました。
解釈間違ってますか？