qpz

base/.gitignore

@@ -0,0 +1,4 @@
+build
+.gradle
+src/main/gen
+src/main/resources/META-INF/native-image

base/src/main/java/org/aya/base/core/AppTerm.java

@@ -5,6 +5,9 @@
 
 public record AppTerm(@NotNull Term fun, @NotNull Term arg) implements Term {
   @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
-    return new AppTerm(fun.bindAt(var, depth), arg.bindAt(var, depth));
+    var newFun = fun.bindAt(var, depth);
+    var newArg = arg.bindAt(var, depth);
+    if (newFun == fun && newArg == arg) return this;
+    return new AppTerm(newFun, newArg);
   }
 }

base/src/main/java/org/aya/base/core/LamTerm.java

@@ -5,6 +5,8 @@
 
 public record LamTerm(Term body) implements Term {
   @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
-    return new LamTerm(body.bindAt(var, depth + 1));
+    var newBody = body.bindAt(var, depth + 1);
+    if (newBody == body) return this;
+    return new LamTerm(newBody);
   }
 }