diff --git a/.github/README.md b/.github/README.md
index 2eb427a93e..f7dae83d1c 100644
--- a/.github/README.md
+++ b/.github/README.md
@@ -43,13 +43,13 @@ Aya is under active development, so please expect bugs, usability or performance
 See also [use as a library](#use-as-a-library).
 
 [GitHub Releases]: https://github.com/aya-prover/aya-dev/releases/tag/nightly-build
-[Java 20]: https://jdk.java.net/20
+[Java 21]: https://jdk.java.net/21
 [1lab]: https://1lab.dev
 
 ## Contributing to Aya
 
-Since you need [Java 20] to set this project up, in case your choice
-of IDE is IntelliJ IDEA, version 2023.2 or higher is required.
+Since you need [Java 21] to set this project up, in case your choice
+of IDE is IntelliJ IDEA, version 2023.3 or higher is required.
 
 + Questions or concerns are welcomed in the discussion area.
   We will try our best to answer your questions, but please be nice.
@@ -104,13 +104,14 @@ implementation group: 'org.aya-prover', name: '[project name]', version: '[lates
 ```
 
 + `[project name]` specifies the subproject of Aya you want to use,
-  and the options are `pretty`, `base`, `cli-impl`, `cli-console`, `parser`, etc.
+  and the options are `pretty`, `base`, `cli-impl`, `parser`, etc.
   + The type checker lives in `base` and `parser`.
   + The generalized pretty printing framework is in `pretty`.
   + The library system, literate mode, single-file type checker, and basic REPL are in `cli-impl`.
-  + The generalized binary operator parser, generalized tree builder,
-    generalized mutable graph, generalized termination checker,
+  + The generalized tree builder, generalized termination checker,
     and a bunch of other utilities (files, etc.) are in `tools`.
+  + The generalized binary operator parser, generalized mutable graph are
+    in `tools-kala` because they depend on a larger subset of the kala library.
   + The command and argument parsing framework is in `tools-repl`.
     It offers an implementation of jline3 parser based on Grammar-Kit and relevant facilities.
   + The literate-markdown related infrastructure is in `tools-md`.
diff --git a/base/build.gradle.kts b/base/build.gradle.kts
index 9781777587..28274b41f2 100644
--- a/base/build.gradle.kts
+++ b/base/build.gradle.kts
@@ -1,10 +1,13 @@
 // Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
-import org.aya.gradle.*
+import org.aya.gradle.CommonTasks
+import org.aya.gradle.GenerateReflectionConfigTask
+import org.aya.gradle.GenerateVersionTask
+
 CommonTasks.nativeImageConfig(project)
 
 dependencies {
-  api(project(":tools"))
+  api(project(":tools-kala"))
   api(project(":tools-md"))
   api(project(":pretty"))
   api(libs.aya.guest0x0)
diff --git a/base/src/main/java/module-info.java b/base/src/main/java/module-info.java
index 2c83038d99..f472005bef 100644
--- a/base/src/main/java/module-info.java
+++ b/base/src/main/java/module-info.java
@@ -2,6 +2,7 @@
   requires transitive aya.md;
   requires transitive aya.pretty;
   requires transitive aya.util;
+  requires transitive aya.util.more;
   requires transitive aya.guest.cubical;
   requires transitive kala.base;
   requires transitive kala.collection;
@@ -15,6 +16,7 @@
   exports org.aya.concrete.error;
   exports org.aya.concrete.remark;
   exports org.aya.concrete.stmt.decl;
+
   exports org.aya.concrete.stmt;
   exports org.aya.concrete.visitor;
   exports org.aya.concrete;
diff --git a/base/src/main/java/org/aya/concrete/Expr.java b/base/src/main/java/org/aya/concrete/Expr.java
index 57afc8dbf6..b659d5de2c 100644
--- a/base/src/main/java/org/aya/concrete/Expr.java
+++ b/base/src/main/java/org/aya/concrete/Expr.java
@@ -28,8 +28,8 @@
 import org.aya.resolve.visitor.ExprResolver;
 import org.aya.resolve.visitor.StmtShallowResolver;
 import org.aya.tyck.Result;
+import org.aya.util.BinOpElem;
 import org.aya.util.ForLSP;
-import org.aya.util.binop.BinOpParser;
 import org.aya.util.error.SourceNode;
 import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
@@ -158,7 +158,7 @@ record App(
    * @author AustinZhu
    */
   record NamedArg(@Override boolean explicit, @Nullable String name, @Override @NotNull Expr term)
-    implements AyaDocile, SourceNode, BinOpParser.Elem<Expr> {
+    implements AyaDocile, SourceNode, BinOpElem<Expr> {
 
     public NamedArg(boolean explicit, @NotNull Expr expr) {
       this(explicit, null, expr);
diff --git a/base/src/main/java/org/aya/concrete/desugar/Desugarer.java b/base/src/main/java/org/aya/concrete/desugar/Desugarer.java
index c8be916672..999635d0d0 100644
--- a/base/src/main/java/org/aya/concrete/desugar/Desugarer.java
+++ b/base/src/main/java/org/aya/concrete/desugar/Desugarer.java
@@ -107,7 +107,7 @@ public static class DesugarInterruption extends Exception {}
         },
         // do not desugar
         right -> arrayExpr);
-      case Expr.LetOpen(var $, var $$, var $$$, var body) -> pre(body);
+      case Expr.LetOpen(_, _, _, var body) -> pre(body);
       case Expr misc -> StmtConsumer.super.pre(misc);
     };
   }
diff --git a/base/src/main/java/org/aya/core/serde/SerTerm.java b/base/src/main/java/org/aya/core/serde/SerTerm.java
index d3e191c643..bced96028d 100644
--- a/base/src/main/java/org/aya/core/serde/SerTerm.java
+++ b/base/src/main/java/org/aya/core/serde/SerTerm.java
@@ -187,7 +187,7 @@ record ConReduceRule(
     public @NotNull Term de(@NotNull DeState state) {
       return new RuleReducer.Con(
         (Shaped.Applicable<Term, CtorDef, TeleDecl.DataCtor>) head.deShape(state),
-        dataArgs().ulift, dataArgs.de(state), conArgs.map(x -> x.de(state))
+        dataArgs.ulift, dataArgs.de(state), conArgs.map(x -> x.de(state))
       );
     }
   }
diff --git a/base/src/main/java/org/aya/core/term/FormulaTerm.java b/base/src/main/java/org/aya/core/term/FormulaTerm.java
index 18f2e2af52..581d4e6f01 100644
--- a/base/src/main/java/org/aya/core/term/FormulaTerm.java
+++ b/base/src/main/java/org/aya/core/term/FormulaTerm.java
@@ -45,9 +45,9 @@ public record FormulaTerm(@NotNull Formula<Term> asFormula) implements Term {
 
   public @NotNull SeqView<Term> view() {
     return switch (asFormula) {
-      case Formula.Conn(var $, var l, var r) -> Seq.of(l, r).view();
+      case Formula.Conn(_, var l, var r) -> Seq.of(l, r).view();
       case Formula.Inv(var i) -> SeqView.of(i);
-      case Formula.Lit<?> $ -> SeqView.empty();
+      case Formula.Lit<?> _ -> SeqView.empty();
     };
   }
 }
diff --git a/base/src/main/java/org/aya/core/term/IntegerTerm.java b/base/src/main/java/org/aya/core/term/IntegerTerm.java
index 0651430db1..29d8447299 100644
--- a/base/src/main/java/org/aya/core/term/IntegerTerm.java
+++ b/base/src/main/java/org/aya/core/term/IntegerTerm.java
@@ -44,7 +44,7 @@ public record IntegerTerm(
     var ctorTele = head().ref().core.selfTele;
     assert ctorTele.sizeEquals(1);
 
-    return ImmutableSeq.of(new Arg<>(new IntegerTerm(repr - 1, recognition, type), ctorTele.first().explicit()));
+    return ImmutableSeq.of(new Arg<>(new IntegerTerm(repr - 1, recognition, type), ctorTele.getFirst().explicit()));
   }
 
   @Override public @NotNull IntegerTerm descent(@NotNull UnaryOperator<Term> f, @NotNull UnaryOperator<Pat> g) {
diff --git a/base/src/main/java/org/aya/generic/Shaped.java b/base/src/main/java/org/aya/generic/Shaped.java
index a814fb155a..8b5c747be0 100644
--- a/base/src/main/java/org/aya/generic/Shaped.java
+++ b/base/src/main/java/org/aya/generic/Shaped.java
@@ -9,7 +9,10 @@
 import org.aya.core.pat.Pat;
 import org.aya.core.repr.CodeShape;
 import org.aya.core.repr.ShapeRecognition;
-import org.aya.core.term.*;
+import org.aya.core.term.DataCall;
+import org.aya.core.term.IntegerTerm;
+import org.aya.core.term.RuleReducer;
+import org.aya.core.term.Term;
 import org.aya.ref.DefVar;
 import org.aya.tyck.unify.TermComparator;
 import org.aya.util.Arg;
@@ -70,8 +73,6 @@ default <O extends AyaDocile> boolean compareUntyped(@NotNull Shaped.Nat<O> othe
     }
 
     @NotNull Shaped.Nat<T> map(@NotNull IntUnaryOperator f);
-
-    // int construct(@NotNull T term);
   }
 
   non-sealed interface List<T extends AyaDocile> extends Inductive<T> {
diff --git a/base/src/main/java/org/aya/prettier/BasePrettier.java b/base/src/main/java/org/aya/prettier/BasePrettier.java
index bd79872973..6944ec2ea3 100644
--- a/base/src/main/java/org/aya/prettier/BasePrettier.java
+++ b/base/src/main/java/org/aya/prettier/BasePrettier.java
@@ -23,8 +23,8 @@
 import org.aya.ref.DefVar;
 import org.aya.ref.LocalVar;
 import org.aya.util.Arg;
+import org.aya.util.BinOpElem;
 import org.aya.util.binop.Assoc;
-import org.aya.util.binop.BinOpParser;
 import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -76,7 +76,7 @@ protected BasePrettier(@NotNull PrettierOptions options) {
 
   public @NotNull Doc visitCalls(
     @Nullable Assoc assoc, @NotNull Doc fn,
-    @NotNull SeqView<? extends BinOpParser.@NotNull Elem<Term>> args,
+    @NotNull SeqView<? extends @NotNull BinOpElem<Term>> args,
     @NotNull Outer outer, boolean showImplicits
   ) {
     return visitCalls(assoc, fn, this::term, outer, args, showImplicits);
@@ -109,9 +109,9 @@ protected BasePrettier(@NotNull PrettierOptions options) {
    */
   <T extends AyaDocile> @NotNull Doc visitCalls(
     @Nullable Assoc assoc, @NotNull Doc fn, @NotNull Fmt<T> fmt, Outer outer,
-    @NotNull SeqView<? extends BinOpParser.@NotNull Elem<@NotNull T>> args, boolean showImplicits
+    @NotNull SeqView<? extends @NotNull BinOpElem<@NotNull T>> args, boolean showImplicits
   ) {
-    var visibleArgs = (showImplicits ? args : args.filter(BinOpParser.Elem::explicit)).toImmutableSeq();
+    var visibleArgs = (showImplicits ? args : args.filter(BinOpElem::explicit)).toImmutableSeq();
     if (visibleArgs.isEmpty()) return assoc != null ? Doc.parened(fn) : fn;
     if (assoc != null) {
       var firstArg = visibleArgs.getFirst();
@@ -137,14 +137,14 @@ protected BasePrettier(@NotNull PrettierOptions options) {
    * @see #visitCalls(Assoc, Doc, Fmt, Outer, SeqView, boolean)
    */
   private <T extends AyaDocile> @NotNull Doc
-  prefix(@NotNull Doc fn, @NotNull Fmt<T> fmt, Outer outer, SeqView<? extends BinOpParser.@NotNull Elem<T>> args) {
+  prefix(@NotNull Doc fn, @NotNull Fmt<T> fmt, Outer outer, SeqView<? extends @NotNull BinOpElem<T>> args) {
     var call = Doc.sep(fn, Doc.sep(args.map(arg ->
       arg(fmt, arg, Outer.AppSpine))));
     // If we're in a spine, add parentheses
     return checkParen(outer, call, Outer.AppSpine);
   }
 
-  public static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull BinOpParser.Elem<T> arg, @NotNull Outer outer) {
+  public static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull BinOpElem<T> arg, @NotNull Outer outer) {
     if (arg.explicit()) return fmt.apply(outer, arg.term());
     return Doc.braced(fmt.apply(Outer.Free, arg.term()));
   }
diff --git a/base/src/main/java/org/aya/prettier/ConcretePrettier.java b/base/src/main/java/org/aya/prettier/ConcretePrettier.java
index 7f27cd4d59..30fae9f105 100644
--- a/base/src/main/java/org/aya/prettier/ConcretePrettier.java
+++ b/base/src/main/java/org/aya/prettier/ConcretePrettier.java
@@ -155,7 +155,7 @@ yield visitCalls(null, fn, (nc, l) -> l.toDoc(options), outer,
       }
       case Expr.Lift expr -> Doc.sep(Seq
         .from(IntRange.closed(1, expr.lift()).iterator()).view()
-        .map($ -> Doc.styled(KEYWORD, Doc.symbol("ulift")))
+        .map(_ -> Doc.styled(KEYWORD, Doc.symbol("ulift")))
         .appended(term(Outer.Lifted, expr.expr())));
       case Expr.PartEl el -> Doc.sep(Doc.symbol("{|"),
         partial(el),
@@ -260,9 +260,9 @@ private Doc partial(Expr.PartEl el) {
   public @NotNull Doc pattern(@NotNull Pattern pattern, boolean licit, Outer outer) {
     return switch (pattern) {
       case Pattern.Tuple tuple -> Doc.licit(licit, patterns(tuple.patterns()));
-      case Pattern.Absurd $ -> Doc.bracedUnless(Doc.styled(KEYWORD, "()"), licit);
+      case Pattern.Absurd _ -> Doc.bracedUnless(Doc.styled(KEYWORD, "()"), licit);
       case Pattern.Bind bind -> Doc.bracedUnless(linkDef(bind.bind()), licit);
-      case Pattern.CalmFace $ -> Doc.bracedUnless(Doc.plain(Constants.ANONYMOUS_PREFIX), licit);
+      case Pattern.CalmFace _ -> Doc.bracedUnless(Doc.plain(Constants.ANONYMOUS_PREFIX), licit);
       case Pattern.Number number -> Doc.bracedUnless(Doc.plain(String.valueOf(number.number())), licit);
       case Pattern.Ctor ctor -> {
         var name = linkRef(ctor.resolved().data(), CON);
@@ -270,7 +270,7 @@ private Doc partial(Expr.PartEl el) {
         yield ctorDoc(outer, licit, ctorDoc, ctor.params().isEmpty());
       }
       case Pattern.QualifiedRef qref -> Doc.bracedUnless(Doc.plain(qref.qualifiedID().join()), licit);
-      case Pattern.BinOpSeq(var pos, var param) -> {
+      case Pattern.BinOpSeq(_, var param) -> {
         if (param.sizeEquals(1)) {
           yield pattern(param.getFirst(), outer);
         }
diff --git a/base/src/main/java/org/aya/prettier/CorePrettier.java b/base/src/main/java/org/aya/prettier/CorePrettier.java
index 80fed17e34..a444171ec4 100644
--- a/base/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/base/src/main/java/org/aya/prettier/CorePrettier.java
@@ -128,7 +128,7 @@ yield visitCalls(null, fn, (nest, t) -> t.toDoc(options), outer,
           options.map.get(AyaPrettierOptions.Key.ShowImplicitArgs)
         );
       }
-      case IntervalTerm $ -> Doc.styled(PRIM, "I");
+      case IntervalTerm _ -> Doc.styled(PRIM, "I");
       case NewTerm(var inner) -> visitCalls(null, Doc.styled(KEYWORD, "new"), (nest, t) -> t.toDoc(options), outer,
         SeqView.of(new Arg<>(o -> term(Outer.AppSpine, inner), true)),
         options.map.get(AyaPrettierOptions.Key.ShowImplicitArgs)
diff --git a/base/src/main/java/org/aya/tyck/unify/TermComparator.java b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
index dc29c78647..a6dc540c38 100644
--- a/base/src/main/java/org/aya/tyck/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
@@ -278,11 +278,11 @@ private boolean doCompareTyped(@NotNull Term type, @NotNull Term lhs, @NotNull T
         }
         yield true;
       }
-      case LamTerm $ -> throw new InternalException("LamTerm is never type");
-      case ConCall $ -> throw new InternalException("ConCall is never type");
-      case TupTerm $ -> throw new InternalException("TupTerm is never type");
-      case NewTerm $ -> throw new InternalException("NewTerm is never type");
-      case ErrorTerm $ -> true;
+      case LamTerm _ -> throw new InternalException("LamTerm is never type");
+      case ConCall _ -> throw new InternalException("ConCall is never type");
+      case TupTerm _ -> throw new InternalException("TupTerm is never type");
+      case NewTerm _ -> throw new InternalException("NewTerm is never type");
+      case ErrorTerm _ -> true;
       case SigmaTerm(var paramsSeq) -> {
         var params = paramsSeq.view();
         for (int i = 1, size = paramsSeq.size(); i <= size; i++) {
diff --git a/base/src/test/java/org/aya/literate/HighlighterTester.java b/base/src/test/java/org/aya/literate/HighlighterTester.java
index 42a5b56d21..af4e000e42 100644
--- a/base/src/test/java/org/aya/literate/HighlighterTester.java
+++ b/base/src/test/java/org/aya/literate/HighlighterTester.java
@@ -91,7 +91,7 @@ public HighlighterTester(@NotNull String sourceCode, @NotNull ImmutableSeq<Highl
 
   public void runTest() {
     var sortedActual = actual.view().distinct().sorted().toImmutableSeq().view();
-    if (sortedActual.getLast() instanceof HighlightInfo.Lit(var $, var kind) && kind == HighlightInfo.LitKind.Eol)
+    if (sortedActual.getLast() instanceof HighlightInfo.Lit(_, var kind) && kind == HighlightInfo.LitKind.Eol)
       // Remove the last Eol
       sortedActual = sortedActual.dropLast(1);
     runTest(sortedActual.toImmutableSeq(), Seq.of(expected));
@@ -120,13 +120,13 @@ public void runTest(@NotNull ImmutableSeq<HighlightInfo> actuals, @NotNull Seq<E
       assertEquals(expectedText, actualText, "at " + sourcePos);
 
       switch (actual) {
-        case HighlightInfo.Lit(var $, var ty)
+        case HighlightInfo.Lit(_, var ty)
           when ty == HighlightInfo.LitKind.Keyword && expected.expected() instanceof ExpectedHighlightType.Keyword -> {
         }
-        case HighlightInfo.Lit(var $, var ty)
+        case HighlightInfo.Lit(_, var ty)
           when ty == HighlightInfo.LitKind.Int && expected.expected() instanceof LitInt -> {
         }
-        case HighlightInfo.Lit(var $, var ty)
+        case HighlightInfo.Lit(_, var ty)
           when ty == HighlightInfo.LitKind.String && expected.expected() instanceof ExpectedHighlightType.LitString -> {
         }
 
@@ -138,7 +138,7 @@ public void runTest(@NotNull ImmutableSeq<HighlightInfo> actuals, @NotNull Seq<E
           when expected.expected() instanceof ExpectedHighlightType.Ref expectedRef ->
           assertRef(sourcePos, ref, expectedRef);
 
-        case HighlightInfo.Err err -> throw new UnsupportedOperationException("TODO");   // TODO
+        case HighlightInfo.Err _ -> throw new UnsupportedOperationException("TODO");   // TODO
 
         default ->
           fail("expected: " + expected.getClass().getSimpleName() + ", but actual: " + actual.getClass().getSimpleName());
@@ -213,7 +213,7 @@ public static void highlightAndTest(@Language("Aya") @NotNull String code, @Null
     Stmt.resolve(stmts, resolveInfo, EmptyModuleLoader.INSTANCE);
 
     var result = SyntaxHighlight.highlight(null, Option.some(sourceFile), stmts)
-      .filterNot(it -> it instanceof HighlightInfo.Lit(var $, var kind)
+      .filterNot(it -> it instanceof HighlightInfo.Lit(_, var kind)
         && ignored.contains(kind));
     new HighlighterTester(code, result, expected).runTest();
   }
diff --git a/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java b/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java
index 31ce957bce..9044fa9c34 100644
--- a/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java
+++ b/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java
@@ -26,8 +26,8 @@
 import org.aya.resolve.error.NameProblem;
 import org.aya.resolve.module.CachedModuleLoader;
 import org.aya.resolve.module.ModuleLoader;
-import org.aya.util.StringUtil;
 import org.aya.util.error.InternalException;
+import org.aya.util.more.StringUtil;
 import org.aya.util.reporter.CountingReporter;
 import org.aya.util.reporter.Reporter;
 import org.aya.util.terck.MutableGraph;
@@ -89,13 +89,13 @@ public static int compile(
     @NotNull Path libraryRoot
   ) throws IOException {
     if (!Files.exists(libraryRoot)) {
-      reporter.reportString("Specified library root does not exist: " + libraryRoot);
+      reporter.reportString(STR."Specified library root does not exist: \{libraryRoot}");
       return 1;
     }
     try {
       return newCompiler(primFactory, reporter, flags, advisor, libraryRoot).start();
     } catch (LibraryConfigData.BadConfig bad) {
-      reporter.reportString("Cannot load malformed library: " + bad.getMessage());
+      reporter.reportString(STR."Cannot load malformed library: \{bad.getMessage()}");
       return 1;
     }
   }
@@ -141,8 +141,8 @@ private void resolveImportsIfNeeded(@NotNull LibrarySource source) throws IOExce
         known.noneMatch(k -> k.moduleName().equals(s.moduleName())));
       known.appendAll(dedup);
     });
-    reporter.reportNest("Done in " + StringUtil.timeToString(
-      System.currentTimeMillis() - startTime), LibraryOwner.DEFAULT_INDENT + 2);
+    reporter.reportNest(STR."Done in \{StringUtil.timeToString(
+        System.currentTimeMillis() - startTime)}", LibraryOwner.DEFAULT_INDENT + 2);
     return depGraph;
   }
 
@@ -188,7 +188,7 @@ private void pretty(ImmutableSeq<LibrarySource> modified) throws IOException {
     });
     // THE BIG GAME
     modified.forEachChecked(src -> {
-      // reportNest("[Pretty] " + QualifiedID.join(src.moduleName()));
+      // reportNest(STR."[Pretty] \{QualifiedID.join(src.moduleName())}");
       var doc = src.pretty(ImmutableSeq.empty(), prettierOptions);
       var text = renderOptions.render(outputTarget, doc, setup);
       var outputFileName = AyaFiles.stripAyaSourcePostfix(src.displayPath().toString()) + outputTarget.fileExt;
@@ -214,7 +214,7 @@ private boolean make() throws IOException {
       owner.addModulePath(dep.outDir());
     }
 
-    reporter.reportString("Compiling " + library.name());
+    reporter.reportString(STR."Compiling \{library.name()}");
     var startTime = System.currentTimeMillis();
     if (anyDepChanged || flags.remake()) {
       owner.librarySources().forEach(this::clearModified);
@@ -231,8 +231,8 @@ private boolean make() throws IOException {
     }
 
     var make = make(modified);
-    reporter.reportNest("Library loaded in " + StringUtil.timeToString(
-      System.currentTimeMillis() - startTime), LibraryOwner.DEFAULT_INDENT + 2);
+    reporter.reportNest(STR."Library loaded in \{StringUtil.timeToString(
+        System.currentTimeMillis() - startTime)}", LibraryOwner.DEFAULT_INDENT + 2);
     pretty(modified);
     return make;
   }
@@ -376,7 +376,7 @@ private void tyckOne(@NotNull LibrarySource file) {
         QualifiedID.join(moduleName), file.displayPath()), LibraryOwner.DEFAULT_INDENT);
       var mod = moduleLoader.load(moduleName);
       if (mod == null || file.resolveInfo().get() == null)
-        throw new InternalException("Unable to load module: " + moduleName);
+        throw new InternalException(STR."Unable to load module: \{moduleName}");
     }
   }
 
diff --git a/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java b/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java
index 4dffda9367..6aea2e5a71 100644
--- a/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java
+++ b/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java
@@ -18,7 +18,6 @@
 import org.aya.concrete.stmt.GeneralizedVar;
 import org.aya.concrete.stmt.Stmt;
 import org.aya.concrete.stmt.decl.ClassDecl;
-import org.aya.concrete.stmt.decl.Decl;
 import org.aya.concrete.stmt.decl.TeleDecl;
 import org.aya.concrete.visitor.StmtFolder;
 import org.aya.core.def.*;
@@ -33,6 +32,7 @@
 import org.aya.ref.GenerateKind;
 import org.aya.ref.LocalVar;
 import org.aya.resolve.context.ModuleName;
+import org.aya.util.error.InternalException;
 import org.aya.util.error.SourceFile;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;
@@ -120,7 +120,7 @@ else if (SPECIAL_SYMBOL.contains(tokenType))
   @Override
   public @NotNull MutableList<HighlightInfo> fold(@NotNull MutableList<HighlightInfo> acc, @NotNull Pattern pat) {
     return switch (pat) {
-      case Pattern.Number(var pos, var $) -> add(acc, LitKind.Int.toLit(pos));
+      case Pattern.Number(var pos, _) -> add(acc, LitKind.Int.toLit(pos));
       default -> StmtFolder.super.fold(acc, pat);
     };
   }
@@ -147,32 +147,32 @@ else if (SPECIAL_SYMBOL.contains(tokenType))
   }
 
   private @NotNull HighlightInfo linkRef(@NotNull SourcePos sourcePos, @NotNull AnyVar var, @Nullable AyaDocile type) {
-    if (var instanceof LocalVar(var $, var $$, GenerateKind.Generalized(var origin)))
+    if (var instanceof LocalVar(var _, var _, GenerateKind.Generalized(var origin)))
       return linkRef(sourcePos, origin, type);
     return kindOf(var).toRef(sourcePos, BasePrettier.linkIdOf(currentFileModule, var), type);
   }
 
   @SuppressWarnings("unused")
   public static @NotNull DefKind kindOf(@NotNull AnyVar var) {
-    record P(Decl decl, GenericDef def) {}
     return switch (var) {
-      case GeneralizedVar ignored -> DefKind.Generalized;
-      case DefVar<?, ?> defVar -> switch (new P(defVar.concrete, defVar.core)) {
-        case P(TeleDecl.FnDecl $, var $$) -> DefKind.Fn;
-        case P(ClassDecl $, var $$) -> DefKind.Clazz;
-        case P(TeleDecl.ClassMember $, var $$) -> DefKind.Member;
-        case P(TeleDecl.DataDecl $, var $$) -> DefKind.Data;
-        case P(TeleDecl.DataCtor $, var $$) -> DefKind.Con;
-        case P(TeleDecl.PrimDecl $, var $$) -> DefKind.Prim;
-        case P(var $, FnDef $$) -> DefKind.Fn;
-        case P(var $, ClassDef $$) -> DefKind.Clazz;
-        case P(var $, MemberDef $$) -> DefKind.Member;
-        case P(var $, DataDef $$) -> DefKind.Data;
-        case P(var $, CtorDef $$) -> DefKind.Con;
-        case P(var $, PrimDef $$) -> DefKind.Prim;
-      };
-      case LocalVar(var $, var $$, GenerateKind.Generalized(var $$$)) -> DefKind.Generalized;
-      case LocalVar ignored -> DefKind.LocalVar;
+      case GeneralizedVar _ -> DefKind.Generalized;
+      case DefVar<?, ?> defVar -> {
+        if (defVar.concrete instanceof TeleDecl.FnDecl || defVar.core instanceof FnDef)
+          yield DefKind.Fn;
+        else if (defVar.concrete instanceof TeleDecl.ClassMember || defVar.core instanceof MemberDef)
+          yield DefKind.Member;
+        else if (defVar.concrete instanceof TeleDecl.DataDecl || defVar.core instanceof DataDef)
+          yield DefKind.Data;
+        else if (defVar.concrete instanceof TeleDecl.DataCtor || defVar.core instanceof CtorDef)
+          yield DefKind.Con;
+        else if (defVar.concrete instanceof TeleDecl.PrimDecl || defVar.core instanceof PrimDef)
+          yield DefKind.Prim;
+        else if (defVar.concrete instanceof ClassDecl || defVar.core instanceof ClassDef)
+          yield DefKind.Clazz;
+        else throw new InternalException(STR."unknown def type: \{defVar}");
+      }
+      case LocalVar(_, _, GenerateKind.Generalized(_)) -> DefKind.Generalized;
+      case LocalVar _ -> DefKind.LocalVar;
       default -> DefKind.Unknown;
     };
   }
diff --git a/cli-impl/src/main/java/org/aya/cli/parse/AyaProducer.java b/cli-impl/src/main/java/org/aya/cli/parse/AyaProducer.java
index c02ea0a464..f77c04c889 100644
--- a/cli-impl/src/main/java/org/aya/cli/parse/AyaProducer.java
+++ b/cli-impl/src/main/java/org/aya/cli/parse/AyaProducer.java
@@ -568,7 +568,7 @@ private interface LicitParser<T> extends BooleanObjBiFunction<GenericNode<?>, T>
           : newBody.childrenOfType(NEW_ARG).map(arg -> {
             var id = newArgField(arg.child(NEW_ARG_FIELD));
             var bindings = arg.childrenOfType(TELE_PARAM_NAME).map(this::teleParamName)
-              .map(b -> b.map($ -> LocalVar.from(b)))
+              .map(b -> b.map(_ -> LocalVar.from(b)))
               .toImmutableSeq();
             var body = expr(arg.child(EXPR));
             return new Expr.Field<>(sourcePosOf(arg), id, bindings, body, MutableValue.create());
diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml
index d7d23d175b..e374082a1d 100644
--- a/gradle/libs.versions.toml
+++ b/gradle/libs.versions.toml
@@ -2,16 +2,16 @@
 # The Version of this project, aka, The Aya Theorem Prover.
 # Remove "-SNAPSHOT" suffix and run gradle publish to release a new version.
 # After that, increase the version number and add "-SNAPSHOT" suffix back for next cycle.
-project = "0.30-SNAPSHOT"
+project = "0.30"
 
 # https://openjdk.org/
-java = "20"
+java = "21"
 
 # https://github.com/JetBrains/java-annotations
 annotations = "24.0.1"
 kala = "0.69.0"
 picocli = "4.7.5"
-build-util = "0.0.20"
+build-util = "0.0.21"
 # https://github.com/graalvm/native-build-tools
 graal-tools = "0.9.28"
 # https://github.com/jline/jline3
@@ -44,6 +44,8 @@ aya-build-util = { group = "org.aya-prover.upstream", name = "build-util", versi
 aya-build-jflex = { group = "org.aya-prover.upstream", name = "build-util-jflex", version.ref = "build-util" }
 aya-guest0x0 = { group = "org.aya-prover.guest0x0", name = "cubical", version.ref = "guest0x0" }
 
+kala-base = { group = "org.glavo.kala", name = "kala-base", version.ref = "kala" }
+kala-collection = { group = "org.glavo.kala", name = "kala-collection", version.ref = "kala" }
 kala-common = { group = "org.glavo.kala", name = "kala-common", version.ref = "kala" }
 
 picocli-runtime = { group = "info.picocli", name = "picocli", version.ref = "picocli" }
diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties
index 3530e0f440..974619d93d 100644
--- a/gradle/wrapper/gradle-wrapper.properties
+++ b/gradle/wrapper/gradle-wrapper.properties
@@ -2,7 +2,7 @@
 # Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.5-bin.zip
 networkTimeout=10000
 validateDistributionUrl=true
 zipStoreBase=GRADLE_USER_HOME
diff --git a/ide-lsp/src/main/java/org/aya/lsp/models/HighlightResult.java b/ide-lsp/src/main/java/org/aya/lsp/models/HighlightResult.java
index 2e935b1215..66a92dfdb5 100644
--- a/ide-lsp/src/main/java/org/aya/lsp/models/HighlightResult.java
+++ b/ide-lsp/src/main/java/org/aya/lsp/models/HighlightResult.java
@@ -64,8 +64,8 @@ public record Symbol(
           case Prim -> Option.some(Kind.PrimRef);
           case Unknown -> Option.none();
         };
-        case HighlightInfo.Lit $ -> Option.none();   // handled by client
-        case HighlightInfo.Err $ -> Option.none(); // handled by client
+        case HighlightInfo.Lit _ -> Option.none();   // handled by client
+        case HighlightInfo.Err _ -> Option.none(); // handled by client
       };
     }
   }
diff --git a/note/early-changelog.md b/note/early-changelog.md
index 51d9e4103d..7775c05f93 100644
--- a/note/early-changelog.md
+++ b/note/early-changelog.md
@@ -2,7 +2,23 @@
 
 This file contains the changelog of the Aya language 0.x.
 
-Upgraded from Java 19 to Java 20.
+## 0.30
+
+Upgraded from Java 19 to Java 21.
+
+New features:
+
++ Improve `Doc` implementation to account for the nested structure for real
++ Improve stability in pattern matching conversion check, pretty print (thanks @dannypsnl)
++ Clean up something related to `Prop`
++ Introduce the "fake literate" language, which allows one to generate beautifully annotated code using Aya's literate backend with custom, naïve syntax highlighting
++ Literate now works with library system
++ Use Gradle version catalog to replace `deps.properties`
++ Introduce `ij-parsing-wrapper` and use it in the parsing code
++ Improve `let` handling
++ Improve "count usages" in language server
++ The new classifier is in `tools` now
++ Loads of build system improvements
 
 Welcome [AliasQli](https://github.com/AliasQli)!
 
diff --git a/pretty/build.gradle.kts b/pretty/build.gradle.kts
index 06e493b690..3f48022355 100644
--- a/pretty/build.gradle.kts
+++ b/pretty/build.gradle.kts
@@ -1,8 +1,8 @@
-// Copyright (c) 2020-2021 Yinsen (Tesla) Zhang.
-// Use of this source code is governed by the MIT license that can be found in the LICENSE file.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 dependencies {
   api(libs.annotations)
-  api(libs.kala.common)
+  api(libs.kala.collection)
   testImplementation(libs.junit.jupiter)
   testImplementation(libs.hamcrest)
 }
diff --git a/pretty/src/main/java/org/aya/pretty/backend/html/Html5Stylist.java b/pretty/src/main/java/org/aya/pretty/backend/html/Html5Stylist.java
index 45ef1064a9..3fd862e513 100644
--- a/pretty/src/main/java/org/aya/pretty/backend/html/Html5Stylist.java
+++ b/pretty/src/main/java/org/aya/pretty/backend/html/Html5Stylist.java
@@ -77,8 +77,8 @@ public ClassedPreset(@NotNull ClosingStylist delegate) {
           case Curly -> "text-decoration-style: wavy;";
         };
         var colorRef = switch (color) {
-          case Style.ColorHex(var rgb, var $) -> cssColor(rgb);
-          case Style.ColorName(var name, var $) -> "var(%s)".formatted(cssVar(name));
+          case Style.ColorHex(var rgb, _) -> cssColor(rgb);
+          case Style.ColorName(var name, _) -> "var(%s)".formatted(cssVar(name));
           case null -> null;
         };
         var decoColor = colorRef != null
diff --git a/pretty/src/main/java/org/aya/pretty/backend/latex/TeXStylist.java b/pretty/src/main/java/org/aya/pretty/backend/latex/TeXStylist.java
index 6270cc6372..21b13e264f 100644
--- a/pretty/src/main/java/org/aya/pretty/backend/latex/TeXStylist.java
+++ b/pretty/src/main/java/org/aya/pretty/backend/latex/TeXStylist.java
@@ -87,7 +87,7 @@ public ClassedPreset(@NotNull ClosingStylist delegate) {
         case Italic -> Tuple.of("\\textit{", "}");
         case Bold -> Tuple.of("\\textbf{", "}");
       };
-      case Style.LineThrough(var pos, var $, var $$) -> switch (pos) {
+      case Style.LineThrough(var pos, _, _) -> switch (pos) {
         case Strike -> Tuple.of("\\sout{", "}");
         case Underline -> Tuple.of("\\underline{", "}");
         case Overline -> null;
diff --git a/pretty/src/main/java/org/aya/pretty/backend/string/StringPrinter.java b/pretty/src/main/java/org/aya/pretty/backend/string/StringPrinter.java
index b66be18c97..5eec6eab13 100644
--- a/pretty/src/main/java/org/aya/pretty/backend/string/StringPrinter.java
+++ b/pretty/src/main/java/org/aya/pretty/backend/string/StringPrinter.java
@@ -112,7 +112,7 @@ protected void renderDoc(@NotNull Cursor cursor, @NotNull Doc doc, EnumSet<Outer
       case Doc.InlineMath inlineMath -> renderInlineMath(cursor, inlineMath, outer);
       case Doc.MathBlock mathBlock -> renderMathBlock(cursor, mathBlock, outer);
       case Doc.Tooltip tooltip -> renderTooltip(cursor, tooltip, outer);
-      case Doc.Empty $ -> {}
+      case Doc.Empty _ -> {}
     }
   }
 
diff --git a/settings.gradle.kts b/settings.gradle.kts
index 7f3e36a622..9ca50af212 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -11,6 +11,8 @@ include(
   "cli-impl",
   "cli-console",
   "tools",
+  // Uses kala-primitives
+  "tools-kala",
   "tools-md",
   "tools-repl",
   "base",
diff --git a/tools-kala/build.gradle.kts b/tools-kala/build.gradle.kts
new file mode 100644
index 0000000000..d01878aa0d
--- /dev/null
+++ b/tools-kala/build.gradle.kts
@@ -0,0 +1,6 @@
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+dependencies {
+  api(libs.kala.common)
+  api(project(":tools"))
+}
diff --git a/tools-kala/src/main/java/module-info.java b/tools-kala/src/main/java/module-info.java
new file mode 100644
index 0000000000..f787616a44
--- /dev/null
+++ b/tools-kala/src/main/java/module-info.java
@@ -0,0 +1,12 @@
+module aya.util.more {
+  requires aya.pretty;
+  requires transitive aya.util;
+
+  requires static org.jetbrains.annotations;
+  requires transitive kala.collection.primitive;
+
+  exports org.aya.util.binop;
+  exports org.aya.util.more;
+  exports org.aya.util.terck;
+  exports org.aya.util.tyck.pat;
+}
diff --git a/tools/src/main/java/org/aya/util/binop/Assoc.java b/tools-kala/src/main/java/org/aya/util/binop/Assoc.java
similarity index 94%
rename from tools/src/main/java/org/aya/util/binop/Assoc.java
rename to tools-kala/src/main/java/org/aya/util/binop/Assoc.java
index a55c1290bc..8168b79d9f 100644
--- a/tools/src/main/java/org/aya/util/binop/Assoc.java
+++ b/tools-kala/src/main/java/org/aya/util/binop/Assoc.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.util.binop;
 
diff --git a/tools/src/main/java/org/aya/util/binop/BinOpParser.java b/tools-kala/src/main/java/org/aya/util/binop/BinOpParser.java
similarity index 98%
rename from tools/src/main/java/org/aya/util/binop/BinOpParser.java
rename to tools-kala/src/main/java/org/aya/util/binop/BinOpParser.java
index 3e238cb48e..0ea58a6211 100644
--- a/tools/src/main/java/org/aya/util/binop/BinOpParser.java
+++ b/tools-kala/src/main/java/org/aya/util/binop/BinOpParser.java
@@ -8,6 +8,7 @@
 import kala.collection.mutable.*;
 import kala.tuple.Tuple;
 import kala.tuple.Tuple2;
+import org.aya.util.BinOpElem;
 import org.aya.util.error.SourceNode;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;
@@ -18,7 +19,7 @@
 public abstract class BinOpParser<
   OpSet extends BinOpSet,
   Expr extends SourceNode,
-  Elm extends BinOpParser.Elem<Expr>> {
+  Elm extends BinOpElem<Expr>> {
   protected final @NotNull OpSet opSet;
   private final @NotNull SeqView<@NotNull Elm> seq;
 
@@ -214,8 +215,4 @@ enum AppliedSide {
     return a.term().sourcePos();
   }
 
-  public interface Elem<Expr> {
-    @NotNull Expr term();
-    boolean explicit();
-  }
 }
diff --git a/tools/src/main/java/org/aya/util/binop/BinOpSet.java b/tools-kala/src/main/java/org/aya/util/binop/BinOpSet.java
similarity index 98%
rename from tools/src/main/java/org/aya/util/binop/BinOpSet.java
rename to tools-kala/src/main/java/org/aya/util/binop/BinOpSet.java
index 70adbc9bad..5711ef697d 100644
--- a/tools/src/main/java/org/aya/util/binop/BinOpSet.java
+++ b/tools-kala/src/main/java/org/aya/util/binop/BinOpSet.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.util.binop;
 
diff --git a/tools/src/main/java/org/aya/util/binop/OpDecl.java b/tools-kala/src/main/java/org/aya/util/binop/OpDecl.java
similarity index 91%
rename from tools/src/main/java/org/aya/util/binop/OpDecl.java
rename to tools-kala/src/main/java/org/aya/util/binop/OpDecl.java
index 74bbed2c42..6d0bd91021 100644
--- a/tools/src/main/java/org/aya/util/binop/OpDecl.java
+++ b/tools-kala/src/main/java/org/aya/util/binop/OpDecl.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.util.binop;
 
diff --git a/tools/src/main/java/org/aya/util/StringUtil.java b/tools-kala/src/main/java/org/aya/util/more/StringUtil.java
similarity index 98%
rename from tools/src/main/java/org/aya/util/StringUtil.java
rename to tools-kala/src/main/java/org/aya/util/more/StringUtil.java
index 74032529f6..e687d09108 100644
--- a/tools/src/main/java/org/aya/util/StringUtil.java
+++ b/tools-kala/src/main/java/org/aya/util/more/StringUtil.java
@@ -1,6 +1,6 @@
 // Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
-package org.aya.util;
+package org.aya.util.more;
 
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
diff --git a/tools/src/main/java/org/aya/util/terck/CallGraph.java b/tools-kala/src/main/java/org/aya/util/terck/CallGraph.java
similarity index 99%
rename from tools/src/main/java/org/aya/util/terck/CallGraph.java
rename to tools-kala/src/main/java/org/aya/util/terck/CallGraph.java
index 2b36a781d2..50ca2d84df 100644
--- a/tools/src/main/java/org/aya/util/terck/CallGraph.java
+++ b/tools-kala/src/main/java/org/aya/util/terck/CallGraph.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.util.terck;
 
diff --git a/tools/src/main/java/org/aya/util/terck/CallMatrix.java b/tools-kala/src/main/java/org/aya/util/terck/CallMatrix.java
similarity index 98%
rename from tools/src/main/java/org/aya/util/terck/CallMatrix.java
rename to tools-kala/src/main/java/org/aya/util/terck/CallMatrix.java
index d37b1e9f7d..0a08d609eb 100644
--- a/tools/src/main/java/org/aya/util/terck/CallMatrix.java
+++ b/tools-kala/src/main/java/org/aya/util/terck/CallMatrix.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.util.terck;
 
diff --git a/tools/src/main/java/org/aya/util/terck/Diagonal.java b/tools-kala/src/main/java/org/aya/util/terck/Diagonal.java
similarity index 71%
rename from tools/src/main/java/org/aya/util/terck/Diagonal.java
rename to tools-kala/src/main/java/org/aya/util/terck/Diagonal.java
index 8114950176..57c1b93e00 100644
--- a/tools/src/main/java/org/aya/util/terck/Diagonal.java
+++ b/tools-kala/src/main/java/org/aya/util/terck/Diagonal.java
@@ -1,23 +1,23 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.util.terck;
 
 import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableList;
+import kala.range.primitive.IntRange;
 import org.aya.pretty.doc.Doc;
 import org.aya.pretty.doc.Docile;
 import org.jetbrains.annotations.NotNull;
 
-import java.util.stream.IntStream;
-
 public record Diagonal<C, T, P>(
   @NotNull CallMatrix<C, T, P> matrix,
   @NotNull ImmutableSeq<Relation> diagonal
 ) implements Docile {
   public static <C, T, P> @NotNull Diagonal<C, T, P> create(@NotNull CallMatrix<C, T, P> matrix) {
     assert matrix.rows() == matrix.cols();
-    var diag = IntStream.range(0, matrix.rows())
-      .mapToObj(i -> matrix.matrix()[i][i])
-      .collect(ImmutableSeq.factory());
+    var diag = IntRange.closedOpen(0, matrix.rows())
+      .mapToObjTo(MutableList.create(), i -> matrix.matrix()[i][i])
+      .toImmutableSeq();
     return new Diagonal<>(matrix, diag);
   }
 
diff --git a/tools/src/main/java/org/aya/util/terck/MutableGraph.java b/tools-kala/src/main/java/org/aya/util/terck/MutableGraph.java
similarity index 98%
rename from tools/src/main/java/org/aya/util/terck/MutableGraph.java
rename to tools-kala/src/main/java/org/aya/util/terck/MutableGraph.java
index 987eb8a979..c241c77ac5 100644
--- a/tools/src/main/java/org/aya/util/terck/MutableGraph.java
+++ b/tools-kala/src/main/java/org/aya/util/terck/MutableGraph.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.util.terck;
 
diff --git a/tools/src/main/java/org/aya/util/terck/Relation.java b/tools-kala/src/main/java/org/aya/util/terck/Relation.java
similarity index 100%
rename from tools/src/main/java/org/aya/util/terck/Relation.java
rename to tools-kala/src/main/java/org/aya/util/terck/Relation.java
diff --git a/tools/src/main/java/org/aya/util/terck/Selector.java b/tools-kala/src/main/java/org/aya/util/terck/Selector.java
similarity index 100%
rename from tools/src/main/java/org/aya/util/terck/Selector.java
rename to tools-kala/src/main/java/org/aya/util/terck/Selector.java
diff --git a/tools/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java b/tools-kala/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java
similarity index 100%
rename from tools/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java
rename to tools-kala/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java
diff --git a/tools/src/main/java/org/aya/util/tyck/pat/Indexed.java b/tools-kala/src/main/java/org/aya/util/tyck/pat/Indexed.java
similarity index 100%
rename from tools/src/main/java/org/aya/util/tyck/pat/Indexed.java
rename to tools-kala/src/main/java/org/aya/util/tyck/pat/Indexed.java
diff --git a/tools/src/main/java/org/aya/util/tyck/pat/PatClass.java b/tools-kala/src/main/java/org/aya/util/tyck/pat/PatClass.java
similarity index 100%
rename from tools/src/main/java/org/aya/util/tyck/pat/PatClass.java
rename to tools-kala/src/main/java/org/aya/util/tyck/pat/PatClass.java
diff --git a/tools-md/build.gradle.kts b/tools-md/build.gradle.kts
index 15fc7fda58..e15af34946 100644
--- a/tools-md/build.gradle.kts
+++ b/tools-md/build.gradle.kts
@@ -1,7 +1,7 @@
 // Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 dependencies {
-  api(project(":tools"))
+  api(project(":tools-kala"))
   api(libs.annotations)
   implementation(libs.aya.commonmark)
   testImplementation(libs.junit.jupiter)
diff --git a/tools-md/src/main/java/module-info.java b/tools-md/src/main/java/module-info.java
index b625525d84..28343be996 100644
--- a/tools-md/src/main/java/module-info.java
+++ b/tools-md/src/main/java/module-info.java
@@ -1,9 +1,11 @@
 module aya.md {
   requires aya.util;
+  requires aya.util.more;
   requires transitive aya.pretty;
 
   requires org.commonmark;
   requires static org.jetbrains.annotations;
+  requires kala.collection.primitive;
 
   exports org.aya.literate;
   exports org.aya.literate.parser;
diff --git a/tools-md/src/main/java/org/aya/literate/parser/BaseMdParser.java b/tools-md/src/main/java/org/aya/literate/parser/BaseMdParser.java
index 10ed4a7d0e..a8e1554d33 100644
--- a/tools-md/src/main/java/org/aya/literate/parser/BaseMdParser.java
+++ b/tools-md/src/main/java/org/aya/literate/parser/BaseMdParser.java
@@ -17,10 +17,10 @@
 import org.aya.pretty.backend.md.MdStyle;
 import org.aya.pretty.doc.Doc;
 import org.aya.pretty.doc.Style;
-import org.aya.util.StringUtil;
 import org.aya.util.error.InternalException;
 import org.aya.util.error.SourceFile;
 import org.aya.util.error.SourcePos;
+import org.aya.util.more.StringUtil;
 import org.aya.util.reporter.Reporter;
 import org.commonmark.node.*;
 import org.commonmark.parser.IncludeSourceSpans;
@@ -89,8 +89,8 @@ public BaseMdParser(@NotNull SourceFile file, @NotNull Reporter reporter, @NotNu
     return switch (node) {
       case Text text -> new Literate.Raw(Doc.plain(text.getLiteral()));
       case Emphasis emphasis -> new Literate.Many(Style.italic(), mapChildren(emphasis));
-      case HardLineBreak $ -> new Literate.Raw(Doc.line());
-      case SoftLineBreak $ -> new Literate.Raw(Doc.line());
+      case HardLineBreak _ -> new Literate.Raw(Doc.line());
+      case SoftLineBreak _ -> new Literate.Raw(Doc.line());
       case StrongEmphasis emphasis -> new Literate.Many(Style.bold(), mapChildren(emphasis));
       case Paragraph p -> new Literate.Many(MdStyle.GFM.Paragraph, mapChildren(p));
       case BlockQuote b -> new Literate.Many(MdStyle.GFM.BlockQuote, mapChildren(b));
@@ -125,7 +125,7 @@ public BaseMdParser(@NotNull SourceFile file, @NotNull Reporter reporter, @NotNu
       case Code inlineCode -> {
         var spans = inlineCode.getSourceSpans();
         if (spans != null && spans.size() == 1) {
-          var sourceSpan = spans.get(0);
+          var sourceSpan = spans.getFirst();
           var lineIndex = linesIndex.get(sourceSpan.getLineIndex());
           var startFrom = lineIndex + sourceSpan.getColumnIndex();
           var sourcePos = fromSourceSpans(file, startFrom, Seq.of(sourceSpan));
diff --git a/tools-repl/build.gradle.kts b/tools-repl/build.gradle.kts
index ef13223abb..5542ccedd5 100644
--- a/tools-repl/build.gradle.kts
+++ b/tools-repl/build.gradle.kts
@@ -1,7 +1,6 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 dependencies {
-  api(project(":pretty"))
   api(project(":tools"))
   api(libs.jline.reader)
   api(libs.jline.terminal.api)
diff --git a/tools/build.gradle.kts b/tools/build.gradle.kts
index fd3a8e52e2..0a26a759d0 100644
--- a/tools/build.gradle.kts
+++ b/tools/build.gradle.kts
@@ -2,7 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 dependencies {
   api(libs.annotations)
-  api(libs.kala.common)
+  api(libs.kala.collection)
   api(project(":pretty"))
   implementation(libs.aya.ij.text)
   testImplementation(libs.junit.jupiter)
diff --git a/tools/src/main/java/module-info.java b/tools/src/main/java/module-info.java
index 6a40a0d8f4..bbb3aa370c 100644
--- a/tools/src/main/java/module-info.java
+++ b/tools/src/main/java/module-info.java
@@ -3,14 +3,11 @@
   requires aya.pretty;
 
   requires static org.jetbrains.annotations;
-  requires transitive kala.collection.primitive;
+  requires transitive kala.collection;
 
-  exports org.aya.util.binop;
   exports org.aya.util.error;
   exports org.aya.util.prettier;
   exports org.aya.util.reporter;
-  exports org.aya.util.terck;
-  exports org.aya.util.tyck.pat;
   exports org.aya.util.tyck;
   exports org.aya.util;
 }
diff --git a/tools/src/main/java/org/aya/util/Arg.java b/tools/src/main/java/org/aya/util/Arg.java
index 6760ca6109..bb261de06e 100644
--- a/tools/src/main/java/org/aya/util/Arg.java
+++ b/tools/src/main/java/org/aya/util/Arg.java
@@ -4,7 +4,6 @@
 
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
-import org.aya.util.binop.BinOpParser;
 import org.jetbrains.annotations.NotNull;
 
 import java.util.function.Consumer;
@@ -16,7 +15,7 @@
  *            In Aya, it is either core term, core pattern, concrete term, or concrete pattern.
  * @author ice1000
  */
-public record Arg<T>(@Override @NotNull T term, @Override boolean explicit) implements BinOpParser.Elem<T> {
+public record Arg<T>(@Override @NotNull T term, @Override boolean explicit) implements BinOpElem<T> {
   public static <T> @NotNull Arg<T> ofExplicitly(@NotNull T term) {
     return new Arg<>(term, true);
   }
diff --git a/tools/src/main/java/org/aya/util/BinOpElem.java b/tools/src/main/java/org/aya/util/BinOpElem.java
new file mode 100644
index 0000000000..c6ef2e3249
--- /dev/null
+++ b/tools/src/main/java/org/aya/util/BinOpElem.java
@@ -0,0 +1,10 @@
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.util;
+
+import org.jetbrains.annotations.NotNull;
+
+public interface BinOpElem<Expr> {
+  @NotNull Expr term();
+  boolean explicit();
+}