finish occursIn

This commit is contained in:
Michael Zhang 2024-07-31 20:55:05 -05:00
parent 102b5efc46
commit 5b5601f5ee

View file

@ -259,6 +259,13 @@ function occursIn(x: variable, e: expr): boolean {
return isEqual(e.x, x);
case "universe":
return false;
case "pi":
case "lambda":
if (occursIn(x, e.abs.type)) return true;
if (!isEqual(e.abs.x, x)) return occursIn(x, e.abs.body);
return false;
case "app":
return occursIn(x, e.left) || occursIn(x, e.right);
}
}