From 5b5601f5ee7dcf0378eb288a33f26436be6c11fd Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 31 Jul 2024 20:55:05 -0500
Subject: [PATCH] finish occursIn

---
 main.ts | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/main.ts b/main.ts
index ef5ef47..2ceaec7 100644
--- a/main.ts
+++ b/main.ts
@@ -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);
   }
 }