misc: add some rubbish

aya-prover · Jun 26, 2024 · ea356a9 · ea356a9
1 parent 76ea37d
commit ea356a9
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java b/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java
@@ -129,6 +129,19 @@ record Locns(@NotNull ImmutableSeq<Param> telescope, @NotNull Term result) imple
       assert count <= telescopeSize();
       return new Locns(telescope.drop(count), result);
     }
+
+    @Override
+    public @NotNull Locns inst(ImmutableSeq<Term> preArgs) {
+      if (preArgs.isEmpty()) return this;
+      assert preArgs.size() <= telescopeSize();
+      var view = preArgs.view();
+      var cope = telescope.view()
+        .drop(preArgs.size())
+        .mapIndexed((idx, p) -> p.descent(t -> t.replaceTeleFrom(idx, view)))
+        .toImmutableSeq();
+      var result = this.result.replaceTeleFrom(cope.size(), view);
+      return new Locns(cope, result);
+    }
   }
 
   record Lift(