pretty: recover some files from TODO due to BasePrettier

base/src/main/java/org/aya/tyck/error/CounterexampleError.java

@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.error;
 
+import org.aya.prettier.BasePrettier;
 import org.aya.pretty.doc.Doc;
 import org.aya.syntax.ref.AnyVar;
 import org.aya.util.error.SourcePos;
@@ -12,8 +13,7 @@ public record CounterexampleError(@Override @NotNull SourcePos sourcePos, @NotNu
   @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
     return Doc.sep(
       Doc.english("The counterexample"),
-      // TODO
-      // BasePrettier.varDoc(var),
+      BasePrettier.varDoc(var),
       Doc.english("does not raise any type error"));
   }
 }

base/src/main/java/org/aya/tyck/error/NobodyError.java

@@ -2,7 +2,16 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.error;
 
-/*public record NobodyError(
+import org.aya.prettier.BasePrettier;
+import org.aya.pretty.doc.Doc;
+import org.aya.syntax.concrete.stmt.decl.TeleDecl;
+import org.aya.syntax.core.def.FnDef;
+import org.aya.syntax.ref.DefVar;
+import org.aya.util.error.SourcePos;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+
+public record NobodyError(
   @Override @NotNull SourcePos sourcePos,
   @NotNull DefVar<FnDef, TeleDecl.FnDecl> var
 ) implements TyckError {
@@ -12,4 +21,4 @@
       BasePrettier.defVar(var),
       Doc.english("does not have a telescope"));
   }
-}*/
+}

syntax/src/main/java/module-info.java

@@ -9,6 +9,7 @@
   requires static org.jetbrains.annotations;
 
   exports org.aya.generic;
+  exports org.aya.prettier;
   exports org.aya.syntax.concrete.stmt.decl;
   exports org.aya.syntax.concrete.stmt;
   exports org.aya.syntax.concrete;