Closed colin-mcd closed 1 year ago
Alpha-renaming doesn't seem to account for global variables currently. For example, this file
data N0 = n0; data N1 = n1; define f0 : N0 -> N1 = \n. case n of n0 -> n1; define f1 : N1 -> N0 = \n. case n of n1 -> n0; n0;
ends up with the line
define f1 : N1 -> N0 = \n0. case n0 of n1 -> n0;"
which is obviously incorrect (and produces a type-checking error). However, if we had started with the line
define f1 : N1 -> N0 = \n'. case n' of n1 -> n0;"
it works without issue.
I'll try to push a fix later.
Alpha-renaming doesn't seem to account for global variables currently. For example, this file
ends up with the line
which is obviously incorrect (and produces a type-checking error). However, if we had started with the line
it works without issue.
I'll try to push a fix later.