pretty: fix altF7

aya-prover · Jan 25, 2025 · 8444d24 · 8444d24
1 parent 7e1ddf5
commit 8444d24
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/syntax/src/main/java/org/aya/prettier/BasePrettier.java b/syntax/src/main/java/org/aya/prettier/BasePrettier.java
@@ -222,10 +222,10 @@ protected static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull Bin
     for (int i = 1; i < telescope.size(); i++) {
       var param = telescope.get(i);
       if (!Objects.equals(param.type(), last.type())) {
-        if (body != null && names.sizeEquals(1)) {
+        if (names.sizeEquals(1)) {
           var ref = names.getFirst();
-          var used = telescope.sliceView(i, telescope.size())
-            .map(ParamLike::type).appended(body)
+          var prefix = telescope.sliceView(i, telescope.size()).map(ParamLike::type);
+          var used = (body == null ? prefix : prefix.appended(body))
             .anyMatch(p -> altF7.applyAsInt(p, ref.ref()) > 0);
           // We omit the name if there is no usage.
           if (!used) buf.append(justType(last, Outer.ProjHead));

diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -340,7 +340,7 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
     var subst = tele.<Term>map(x -> new FreeTerm(x.ref()));
     var result = telescope.result(subst);
 
-    line1.append(visitTele(tele, result));
+    line1.append(visitTele(tele));
     line1.append(HAS_TYPE);
     line1.append(term(Outer.Free, result));