Can't apply a substitution when there are invalid substitutions
Closed this issue · 1 comments
CatsAreFluffy commented
When the unifier finds an invalid substitution, you can't apply a substitution, even if a valid substitution exists. A simple case with this problem is unifying |- E. x e. D ph with |- E. x e. A B = C.
CatsAreFluffy commented
Doesn't happen in the current dev version. Closing.