In infer mode, type inference is happening and Infer%s will be resolved, if possible.
Also, two free but different Var%s are considered α-equivalent.
When *not in infer mode, no type inference is happening and Infer%s will not be touched.
Also, Two free but different Var%s are not considered α-equivalent.
In addition:
tuples/sigma are now converted to packs/arrs modulo α-equivalence:
Alpha-Equivalence checks now knows two modes:
infermode, type inference is happening and Infer%s will be resolved, if possible. Also, two free but different Var%s are considered α-equivalent.infermode, no type inference is happening and Infer%s will not be touched. Also, Two free but different Var%s are not considered α-equivalent.In addition:
(a, a')=>‹2; a›[A, A']=>«2; A»