Fix α-normalization bug (#319)
This fixes α-normalization to correctly relabel a `let`-bound variable
This commit is contained in:
parent
bd83658409
commit
99c6241111
|
@ -890,7 +890,7 @@ alphaNormalize (App f₀ a₀) =
|
|||
|
||||
a₁ = alphaNormalize a₀
|
||||
alphaNormalize (Let x (Just _A₀) a₀ b₀) =
|
||||
Let x (Just _A₁) a₁ b₃
|
||||
Let "_" (Just _A₁) a₁ b₃
|
||||
where
|
||||
_A₁ = alphaNormalize _A₀
|
||||
|
||||
|
@ -902,7 +902,7 @@ alphaNormalize (Let x (Just _A₀) a₀ b₀) =
|
|||
b₂ = shift (-1) (V x 0) b₁
|
||||
b₃ = alphaNormalize b₂
|
||||
alphaNormalize (Let x Nothing a₀ b₀) =
|
||||
Let x Nothing a₁ b₃
|
||||
Let "_" Nothing a₁ b₃
|
||||
where
|
||||
a₁ = alphaNormalize a₀
|
||||
|
||||
|
|
Loading…
Reference in New Issue
Block a user