diff --git a/base/src/main/java/org/aya/core/pat/PatUnify.java b/base/src/main/java/org/aya/core/pat/PatUnify.java
index 252168c24..dafda0455 100644
--- a/base/src/main/java/org/aya/core/pat/PatUnify.java
+++ b/base/src/main/java/org/aya/core/pat/PatUnify.java
@@ -84,7 +84,7 @@ private void visitAs(@NotNull LocalVar as, Pat rhs) {
 
   private void reportError(@NotNull Pat lhs, @NotNull Pat pat) {
     var doc = Doc.sep(lhs.toDoc(AyaPrettierOptions.debug()), Doc.plain("and"), pat.toDoc(AyaPrettierOptions.debug()));
-    throw new InternalException(doc.debugRender() + " are patterns of different types!");
+    throw new InternalException(STR."\{doc.debugRender()} are patterns of different types!");
   }
 
   private static void unifyPat(Pat lhs, Pat rhs, Subst lhsSubst, Subst rhsSubst, LocalCtx ctx) {
diff --git a/base/src/main/java/org/aya/core/term/Term.java b/base/src/main/java/org/aya/core/term/Term.java
index 6d0b8b839..fe03e6f3f 100644
--- a/base/src/main/java/org/aya/core/term/Term.java
+++ b/base/src/main/java/org/aya/core/term/Term.java
@@ -19,7 +19,6 @@
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.AnyVar;
 import org.aya.ref.LocalVar;
-import org.aya.tyck.env.LocalCtx;
 import org.aya.tyck.tycker.TyckState;
 import org.aya.tyck.unify.Synthesizer;
 import org.aya.util.Arg;
@@ -50,7 +49,7 @@ public sealed interface Term extends AyaDocile, Restr.TermLike<Term>
   permits Callable, CoeTerm, Elimination, Formation, FormulaTerm, HCompTerm, InTerm, MatchTerm, MetaLitTerm, MetaPatTerm, PartialTerm, RefTerm, RefTerm.Field, StableWHNF {
   /**
    * Descending an operation to the term AST. NOTE: Currently we require the operation `f` to preserve:
-   * {@link StructCall}, {@link DataCall}, {@link SortTerm}, {@link org.aya.generic.Shaped.Applicable}.
+   * {@link ClassCall}, {@link DataCall}, {@link SortTerm}, {@link org.aya.generic.Shaped.Applicable}.
    */
   @NotNull Term descent(@NotNull UnaryOperator<Term> f, @NotNull UnaryOperator<Pat> g);
 
@@ -114,13 +113,6 @@ default VarConsumer.ScopeChecker scopeCheck(@NotNull ImmutableSeq<LocalVar> allo
   default @NotNull Term lift(int ulift) {
     return new EndoTerm.Elevator(ulift).apply(this);
   }
-  /**
-   * @return WHNF
-   * @throws NullPointerException if the term is an introduction rule
-   */
-  default @NotNull Term computeType(@NotNull TyckState state, @NotNull LocalCtx ctx) {
-    return new Synthesizer(state, ctx).press(this);
-  }
 
   /**
    * @author re-xyr
diff --git a/base/src/main/java/org/aya/core/visitor/BetaExpander.java b/base/src/main/java/org/aya/core/visitor/BetaExpander.java
index 04ba749a1..4ed72446d 100644
--- a/base/src/main/java/org/aya/core/visitor/BetaExpander.java
+++ b/base/src/main/java/org/aya/core/visitor/BetaExpander.java
@@ -56,24 +56,24 @@ yield switch (partial(partial)) {
       case PartialTerm(var partial, var rhsTy) -> new PartialTerm(partial(partial), rhsTy);
       // TODO[coe]: temporary hack
       case CoeTerm(
-        var ty,
+        _,
         FormulaTerm(Formula.Lit(var r)),
         FormulaTerm(Formula.Lit(var s))
       ) when r == s -> identity("x");
-      case CoeTerm(var ty, RefTerm(var r), RefTerm(var s)) when r == s -> identity("x");
+      case CoeTerm(_, RefTerm(var r), RefTerm(var s)) when r == s -> identity("x");
       case CoeTerm coe -> {
         var varI = new LamTerm.Param(new LocalVar("i"), true);
         var codom = apply(AppTerm.make(coe.type(), varI.toArg()));
 
         yield switch (codom) {
-          case PathTerm path -> term;
+          case PathTerm _ -> term;
           case PiTerm pi -> pi.coe(coe, varI);
           case SigmaTerm sigma -> sigma.coe(coe, varI);
           case DataCall data when data.args().isEmpty() -> identity(String.valueOf(data.ref()
             .name().chars()
             .filter(Character::isAlphabetic)
             .findFirst()).toLowerCase(Locale.ROOT));
-          case SortTerm type -> identity("A");
+          case SortTerm _ -> identity("A");
           default -> term;
         };
       }
diff --git a/base/src/main/java/org/aya/prettier/Codifier.java b/base/src/main/java/org/aya/prettier/Codifier.java
index 5be80302f..6533676e8 100644
--- a/base/src/main/java/org/aya/prettier/Codifier.java
+++ b/base/src/main/java/org/aya/prettier/Codifier.java
@@ -101,9 +101,9 @@ case FormulaTerm(var mula) -> {
         formula(mula);
         builder.append(")");
       }
-      case ErrorTerm error -> throw new UnsupportedOperationException("Cannot generate error");
-      case Callable call -> throw new UnsupportedOperationException("Cannot generate calls");
-      case IntervalTerm interval -> builder.append("IntervalTerm.INSTANCE");
+      case ErrorTerm _ -> throw new UnsupportedOperationException("Cannot generate error");
+      case Callable _ -> throw new UnsupportedOperationException("Cannot generate calls");
+      case IntervalTerm _ -> builder.append("IntervalTerm.INSTANCE");
       case SortTerm sort -> {
         builder.append("new SortTerm(SortKind.");
         builder.append(sort.kind().name());
@@ -111,7 +111,7 @@ case FormulaTerm(var mula) -> {
         builder.append(sort.lift());
         builder.append(")");
       }
-      default -> throw new UnsupportedOperationException("TODO: " + term.getClass().getCanonicalName());
+      default -> throw new UnsupportedOperationException(STR."TODO: \{term.getClass().getCanonicalName()}");
     }
   }
 
diff --git a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
index e0880bd5e..ffc55073a 100644
--- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
+++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
@@ -256,7 +256,7 @@ private void addReference(@NotNull DefVar<?, ?> defVar) {
               addReference(maybe);
               yield new Pattern.Ctor(bind, maybe);
             }
-            ctx.set(ctx.get().bind(bind.bind(), var -> false));
+            ctx.set(ctx.get().bind(bind.bind(), _ -> false));
             yield bind;
           }
           case Pattern.QualifiedRef qref -> {
diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index 6cf178c3f..3dd8d52db 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -174,7 +174,7 @@ yield switch (whnf(term)) {
             return new Result.Default(new RefTerm(loc), ty);
           });
         case DefVar<?, ?> defVar -> inferRef(defVar);
-        default -> throw new InternalException("Unknown var: " + ref.resolvedVar().getClass());
+        default -> throw new InternalException(STR."Unknown var: \{ref.resolvedVar().getClass()}");
       };
       case Expr.Pi pi -> {
         var corePi = ty(pi);
@@ -253,7 +253,7 @@ yield switch (whnf(term)) {
         yield new Result.Default(TupTerm.explicits(items.map(Result::wellTyped)),
           new SigmaTerm(items.map(item -> new Term.Param(LocalVar.IGNORED, item.type(), true))));
       }
-      case Expr.App(var sourcePos, var appF, var argument) -> {
+      case Expr.App(_, var appF, var argument) -> {
         var f = synthesize(appF);
         var app = f.wellTyped();
         if (app instanceof ErrorTerm || f.type() instanceof ErrorTerm) yield f;
@@ -324,7 +324,7 @@ yield switch (whnf(term)) {
         var defs = shapeFactory.findImpl(AyaShape.NAT_SHAPE);
         if (defs.isEmpty()) yield fail(expr, new NoRuleError(expr, null));
         if (defs.sizeGreaterThan(1)) {
-          var type = ctx.freshTyHole("_ty" + lit.integer() + "'", lit.sourcePos());
+          var type = ctx.freshTyHole(STR."_ty\{lit.integer()}'", lit.sourcePos());
           yield new Result.Default(new MetaLitTerm(lit.sourcePos(), lit.integer(), defs, type.component1()), type.component1());
         }
         var match = defs.getFirst();
@@ -558,7 +558,7 @@ private static class ClauseTyckState {
       var field = (DefVar<MemberDef, TeleDecl.ClassMember>) var;
       return new Result.Default(new RefTerm.Field(field), Def.defType(field));
     } else {
-      final var msg = "Def var `" + var.name() + "` has core `" + var.core + "` which we don't know.";
+      final var msg = STR."Def var `\{var.name()}` has core `\{var.core}` which we don't know.";
       throw new InternalException(msg);
     }
   }
@@ -584,14 +584,13 @@ private static boolean needImplicitParamIns(@NotNull Expr expr) {
     return expr instanceof Expr.Lambda ex && ex.param().explicit() || !(expr instanceof Expr.Lambda);
   }
 
-  @SuppressWarnings("unchecked")
   private @Nullable Result inferShapedFn(@NotNull DefVar<FnDef, TeleDecl.FnDecl> var) {
     var recog = shapeFactory.find(var.core);
 
     if (recog.isDefined()) {
       var head = ShapeFactory.ofFn(var, recog.get());
       assert head != null : "bad ShapeFactory";
-      return defCall(var, (defVar, ulift, args) -> new RuleReducer.Fn(head, ulift, args));
+      return defCall(var, (_, ulift, args) -> new RuleReducer.Fn(head, ulift, args));
     }
 
     return null;
@@ -604,7 +603,7 @@ private static boolean needImplicitParamIns(@NotNull Expr expr) {
         if (recog.shape() == AyaShape.NAT_SHAPE) {
           var head = ShapeFactory.ofCtor(var, recog, new DataCall(dataVar, 0, ImmutableSeq.empty()));
           assert head != null : "bad ShapeFactory";
-          return defCall(var, (mVar, ulift, args) -> new RuleReducer.Con(head, ulift, ImmutableSeq.empty(), args));
+          return defCall(var, (_, ulift, args) -> new RuleReducer.Con(head, ulift, ImmutableSeq.empty(), args));
         }
 
         return null;
diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index 0f07d71de..5e508ea82 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -158,7 +158,7 @@ record Tmp(ImmutableSeq<TeleResult> okTele, Term preresult, Term prebody) {}
   }
 
   public void tyckHeader(@NotNull Decl decl, @NotNull ExprTycker tycker) {
-    tracing(builder -> builder.shift(new Trace.LabelT(decl.sourcePos(), "telescope of " + decl.ref().name())));
+    tracing(builder -> builder.shift(new Trace.LabelT(decl.sourcePos(), STR."telescope of \{decl.ref().name()}")));
     switch (decl) {
       case ClassDecl clazz -> {
         var body = clazz.members.map(field -> (MemberDef) tyck(field, tycker));
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 a6dc540c3..e83ce488d 100644
--- a/base/src/main/java/org/aya/tyck/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
@@ -256,7 +256,6 @@ private boolean visitLists(SeqView<Term> l, SeqView<Term> r, Sub lr, Sub rl, @No
     else return null;
   }
 
-  @SuppressWarnings("unused")
   private boolean doCompareTyped(@NotNull Term type, @NotNull Term lhs, @NotNull Term rhs, Sub lr, Sub rl) {
     // Skip tracing, because too easy.
     // Note that it looks tempting to apply some unification here, but it is not correct:
@@ -298,23 +297,22 @@ case SigmaTerm(var paramsSeq) -> {
       // https://stackoverflow.com/q/75971020/7083401
       case PiTerm pi -> ctx.with(pi.param(), () -> {
         var pair = new Pair<>(lhs, rhs);
-        if (pair instanceof Pair(LamTerm(var lp, var lb), LamTerm(var rp, var rb))) {
-          var ref = pi.param().ref();
-          if (ref == LocalVar.IGNORED) ref = new LocalVar(lp.ref().name() + rp.ref().name());
-          lr.map.put(ref, rp.toTerm());
-          rl.map.put(ref, lp.toTerm());
-          var piParam = new RefTerm(ref);
-          var res = compare(lb.subst(lp.ref(), piParam), rb.subst(rp.ref(), piParam), lr, rl, pi.body());
-          lr.map.remove(ref);
-          rl.map.remove(ref);
-          return res;
-        } else if (pair instanceof Pair(var $, LamTerm rambda)) {
-          return compareLambdaBody(rambda, lhs, rl, lr, pi);
-        } else if (pair instanceof Pair(LamTerm lambda, var $)) {
-          return compareLambdaBody(lambda, rhs, lr, rl, pi);
-        } else {
-          return compare(lhs, rhs, lr, rl, null);
-        }
+        return switch (pair) {
+          case Pair(LamTerm(var lp, var lb), LamTerm(var rp, var rb)) -> {
+            var ref = pi.param().ref();
+            if (ref == LocalVar.IGNORED) ref = new LocalVar(lp.ref().name() + rp.ref().name());
+            lr.map.put(ref, rp.toTerm());
+            rl.map.put(ref, lp.toTerm());
+            var piParam = new RefTerm(ref);
+            var res = compare(lb.subst(lp.ref(), piParam), rb.subst(rp.ref(), piParam), lr, rl, pi.body());
+            lr.map.remove(ref);
+            rl.map.remove(ref);
+            yield res;
+          }
+          case Pair(_, LamTerm rambda) -> compareLambdaBody(rambda, lhs, rl, lr, pi);
+          case Pair(LamTerm lambda, _) -> compareLambdaBody(lambda, rhs, lr, rl, pi);
+          default -> compare(lhs, rhs, lr, rl, null);
+        };
       });
       // In this case, both sides have the same type (I hope)
       case PathTerm cube -> ctx.withIntervals(cube.params().view(), () -> {
@@ -376,7 +374,7 @@ private boolean comparePartial(
   ) {
     return switch (new Pair<>(lhs.partial(), rhs.partial())) {
       case Pair(Partial.Const(var ll), Partial.Const(var rr)) -> compare(ll, rr, lr, rl, type.type());
-      case Pair(Partial.Split<?> ll, Partial.Split<?> rr) -> CofThy.conv(type.restr(), new Subst(),
+      case Pair(Partial.Split<?> _, Partial.Split<?> _) -> CofThy.conv(type.restr(), new Subst(),
         subst -> compare(lhs.subst(subst), rhs.subst(subst), lr, rl, type.subst(subst)));
       default -> false;
     };
@@ -414,12 +412,12 @@ case Pair(PiTerm(var lParam, var lBody), PiTerm(var rParam, var rBody)) ->
         checkParam(lParam, rParam, new Subst(), new Subst(), lr, rl, () -> false,
           (lsub, rsub) -> compare(lBody.subst(lsub), rBody.subst(rsub), lr, rl, null));
       case Pair(SigmaTerm(var lParams), SigmaTerm(var rParams)) -> checkParams(lParams.view(), rParams.view(),
-        new Subst(), new Subst(), lr, rl, () -> false, (lsub, rsub) -> true);
+        new Subst(), new Subst(), lr, rl, () -> false, (_, _) -> true);
       case Pair(SortTerm lhs, SortTerm rhs) -> compareSort(lhs, rhs);
       case Pair(PartialTyTerm(var lTy, var lR), PartialTyTerm(var rTy, var rR)) ->
         compare(lTy, rTy, lr, rl, null) && compareRestr(lR, rR);
       case Pair(PathTerm lCube, PathTerm rCube) -> compareCube(lCube, rCube, lr, rl);
-      case Pair(IntervalTerm lhs, IntervalTerm rhs) -> true;
+      case Pair(IntervalTerm _, IntervalTerm _) -> true;
       default -> throw noRules(preLhs);
     };
   }
@@ -474,7 +472,7 @@ case AppTerm(var lOf, var lArg) -> {
         else yield null;
       }
       // See compareApprox for why we don't compare these
-      case FnCall lhs -> null;
+      case FnCall _ -> null;
       case CoeTerm coe -> {
         if (!(preRhs instanceof CoeTerm(var rType, var rR, var rS))) yield null;
         if (!compare(coe.r(), rR, lr, rl, IntervalTerm.INSTANCE)) yield null;
@@ -501,7 +499,7 @@ yield compare(coe.type(), rType, lr, rl, PrimDef.intervalToType()) ?
         default -> null;
       };
       // end ConCallLike
-      case PrimCall lhs -> null;
+      case PrimCall _ -> null;
       case FieldTerm lhs -> {
         if (!(preRhs instanceof FieldTerm rhs)) yield null;
         var preStructType = compareUntyped(lhs.of(), rhs.of(), lr, rl);
@@ -510,8 +508,8 @@ yield compare(coe.type(), rType, lr, rl, PrimDef.intervalToType()) ?
         yield Def.defResult(lhs.ref());
       }
       // We expect to only compare the elimination "outS" here
-      case OutTerm(var lPhi, var pal, var lU) -> {
-        if (!(preRhs instanceof OutTerm(var rPhi, var par, var rU))) yield null;
+      case OutTerm(var lPhi, _, var lU) -> {
+        if (!(preRhs instanceof OutTerm(var rPhi, _, var rU))) yield null;
         if (!compare(lPhi, rPhi, lr, rl, IntervalTerm.INSTANCE)) yield null;
         var innerTy = compareUntyped(lU, rU, lr, rl);
         if (innerTy == null) yield null;
diff --git a/base/src/test/java/org/aya/literate/AyaMdParserTest.java b/base/src/test/java/org/aya/literate/AyaMdParserTest.java
index 69de467f8..59d2d62db 100644
--- a/base/src/test/java/org/aya/literate/AyaMdParserTest.java
+++ b/base/src/test/java/org/aya/literate/AyaMdParserTest.java
@@ -97,7 +97,7 @@ public void testExtract(String caseName) throws IOException {
     var expPath = oneCase.expectedAyaFile();
 
     if (!expPath.toFile().exists()) {
-      System.err.println("Test Data " + expPath + " doesn't exist, skip.");
+      System.err.println(STR."Test Data \{expPath} doesn't exist, skip.");
     } else {
       var expAyaFile = file(expPath);
 
diff --git a/base/src/test/java/org/aya/literate/HighlighterTester.java b/base/src/test/java/org/aya/literate/HighlighterTester.java
index af4e000e4..dff3fdd72 100644
--- a/base/src/test/java/org/aya/literate/HighlighterTester.java
+++ b/base/src/test/java/org/aya/literate/HighlighterTester.java
@@ -117,7 +117,7 @@ public void runTest(@NotNull ImmutableSeq<HighlightInfo> actuals, @NotNull Seq<E
       var expectedText = expected.expected.display();
       var actualText = sourceCode.substring(sourcePos.tokenStartIndex(), sourcePos.tokenEndIndex() + 1);
 
-      assertEquals(expectedText, actualText, "at " + sourcePos);
+      assertEquals(expectedText, actualText, STR."at \{sourcePos}");
 
       switch (actual) {
         case HighlightInfo.Lit(_, var ty)
@@ -141,7 +141,7 @@ public void runTest(@NotNull ImmutableSeq<HighlightInfo> actuals, @NotNull Seq<E
         case HighlightInfo.Err _ -> throw new UnsupportedOperationException("TODO");   // TODO
 
         default ->
-          fail("expected: " + expected.getClass().getSimpleName() + ", but actual: " + actual.getClass().getSimpleName());
+          fail(STR."expected: \{expected.getClass().getSimpleName()}, but actual: \{actual.getClass().getSimpleName()}");
       }
     });
     assertEquals(expecteds.size(), actuals.size(), "size mismatch");
@@ -152,7 +152,7 @@ public void runTest(@NotNull ImmutableSeq<HighlightInfo> actuals, @NotNull Seq<E
    */
   public void checkDef(@NotNull SourcePos sourcePos, @NotNull HighlightInfo.Def def) {
     var existDef = defSet.containsKey(def.target());
-    assertFalse(existDef, "Duplicated def: " + def.target() + " at " + sourcePos);
+    assertFalse(existDef, STR."Duplicated def: \{def.target()} at \{sourcePos}");
 
     defSet.put(def.target(), Option.ofNullable(def.kind()));
   }
@@ -166,7 +166,7 @@ public void assertDef(@NotNull SourcePos sourcePos, @NotNull HighlightInfo.Def a
 
     if (name != null) {
       var existName = defMap.getOption(name);
-      assertFalse(existName.isDefined(), "Duplicated name: " + expectedDef.name());
+      assertFalse(existName.isDefined(), STR."Duplicated name: \{expectedDef.name()}");
 
       defMap.put(name, Tuple.of(actualDef.target(), Option.ofNullable(actualDef.kind())));
     }
@@ -178,7 +178,7 @@ public void assertDef(@NotNull SourcePos sourcePos, @NotNull HighlightInfo.Def a
   public void checkRef(@NotNull SourcePos sourcePos, @NotNull HighlightInfo.Ref ref) {
     var defData = defSet.getOrNull(ref.target());
 
-    assertNotNull(defData, "Expected def: " + ref.target() + " at " + sourcePos);
+    assertNotNull(defData, STR."Expected def: \{ref.target()} at \{sourcePos}");
     assertEquals(defData.getOrNull(), ref.kind());
   }
 
@@ -189,7 +189,7 @@ public void assertRef(@NotNull SourcePos sourcePos, @NotNull HighlightInfo.Ref a
 
     if (name != null) {
       var existName = defMap.getOption(name);
-      assertTrue(existName.isDefined(), "Undefined name: " + expectedRef.name());
+      assertTrue(existName.isDefined(), STR."Undefined name: \{expectedRef.name()}");
 
       var defData = existName.get();
       assertEquals(defData.component2().getOrNull(), actualRef.kind());
diff --git a/base/src/test/java/org/aya/test/TestRunner.java b/base/src/test/java/org/aya/test/TestRunner.java
index 0e09da1b7..acbcfea3d 100644
--- a/base/src/test/java/org/aya/test/TestRunner.java
+++ b/base/src/test/java/org/aya/test/TestRunner.java
@@ -47,7 +47,7 @@ public class TestRunner {
    * For running single test, use the main() function below.
    */
   @Test void runAllAyaTests() {
-    System.out.println("Aya Test Runner: Running for commit " + GeneratedVersion.COMMIT_HASH);
+    System.out.println(STR."Aya Test Runner: Running for commit \{GeneratedVersion.COMMIT_HASH}");
     runDir(DEFAULT_TEST_DIR.resolve("failure"), false);
   }
 
@@ -57,14 +57,14 @@ public static void main(String[] args) {
     Arrays.stream(args).map(Paths::get).forEach(path -> {
       if (Files.isRegularFile(path)) runner.runFile(path, true);
       else if (Files.isDirectory(path)) runner.runDir(path, true);
-      else if (Files.notExists(path)) fail("Test target not found: " + path.toAbsolutePath());
-      else fail("Unsupported test target: " + path.toAbsolutePath());
+      else if (Files.notExists(path)) fail(STR."Test target not found: \{path.toAbsolutePath()}");
+      else fail(STR."Unsupported test target: \{path.toAbsolutePath()}");
     });
     TestRunner.exit();
   }
 
   private void runDir(@NotNull Path path, boolean expectSuccess) {
-    System.out.println(":: Running tests under " + path.toAbsolutePath());
+    System.out.println(STR.":: Running tests under \{path.toAbsolutePath()}");
     assertTrue(path.toFile().isDirectory(), "should be a directory");
 
     var source = AyaFiles.collectAyaSourceFiles(path);
@@ -78,13 +78,13 @@ private void runFile(@NotNull Path file, boolean expectSuccess) {
       var reporter = CountingReporter.delegate(new StreamReporter(new PrintStream(
         hookOut, true, StandardCharsets.UTF_8)));
 
-      System.out.print(file.getFileName() + " ---> ");
+      System.out.print(STR."\{file.getFileName()} ---> ");
       new SingleFileCompiler(reporter, LOCATOR, null)
         .compile(file, flags(), null);
 
       postRun(file, expectSuccess, hookOut.toString(StandardCharsets.UTF_8), reporter);
     } catch (IOException e) {
-      fail("error reading file " + file.toAbsolutePath());
+      fail(STR."error reading file \{file.toAbsolutePath()}");
     }
   }
 
@@ -95,7 +95,7 @@ private void runFile(@NotNull Path file, boolean expectSuccess) {
   }
 
   private void postRun(@NotNull Path file, boolean expectSuccess, String output, CountingReporter reporter) {
-    var expectedOutFile = file.resolveSibling(file.getFileName() + ".txt");
+    var expectedOutFile = file.resolveSibling(STR."\{file.getFileName()}.txt");
     if (Files.exists(expectedOutFile)) {
       checkOutput(file, expectedOutFile, output);
       System.out.println("success");
@@ -112,7 +112,7 @@ private void postRun(@NotNull Path file, boolean expectSuccess, String output, C
               ----------------------------------------
               """,
             output);
-          fail("The test case <" + file.getFileName() + "> should pass, but it fails.");
+          fail(STR."The test case <\{file.getFileName()}> should pass, but it fails.");
         }
       } else {
         System.out.println(); // add line break after `--->`
@@ -123,11 +123,11 @@ private void postRun(@NotNull Path file, boolean expectSuccess, String output, C
 
   private void generateWorkflow(@NotNull Path testFile, Path expectedOutFile, String hookOut) {
     hookOut = instantiateHoles(testFile, hookOut);
-    var workflowFile = testFile.resolveSibling(testFile.getFileName() + ".txt");
+    var workflowFile = testFile.resolveSibling(STR."\{testFile.getFileName()}.txt");
     try {
       FileUtil.writeString(workflowFile, hookOut);
     } catch (IOException e) {
-      fail("error generating todo file " + workflowFile.toAbsolutePath());
+      fail(STR."error generating todo file \{workflowFile.toAbsolutePath()}");
     }
     System.out.printf(Locale.getDefault(),
       """
@@ -150,7 +150,7 @@ private void checkOutput(@NotNull Path testFile, Path expectedOutFile, String ho
         Files.readString(expectedOutFile, StandardCharsets.UTF_8)));
       assertEquals(expected, output, testFile.getFileName().toString());
     } catch (IOException e) {
-      fail("error reading file " + expectedOutFile.toAbsolutePath());
+      fail(STR."error reading file \{expectedOutFile.toAbsolutePath()}");
     }
   }
 
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 6aea2e5a7..4cdb3237e 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
@@ -152,7 +152,6 @@ else if (SPECIAL_SYMBOL.contains(tokenType))
     return kindOf(var).toRef(sourcePos, BasePrettier.linkIdOf(currentFileModule, var), type);
   }
 
-  @SuppressWarnings("unused")
   public static @NotNull DefKind kindOf(@NotNull AnyVar var) {
     return switch (var) {
       case GeneralizedVar _ -> DefKind.Generalized;
diff --git a/cli-impl/src/test/java/org/aya/cli/LibraryGraphTest.java b/cli-impl/src/test/java/org/aya/cli/LibraryGraphTest.java
index 4e25379f4..e42e1cac9 100644
--- a/cli-impl/src/test/java/org/aya/cli/LibraryGraphTest.java
+++ b/cli-impl/src/test/java/org/aya/cli/LibraryGraphTest.java
@@ -2,7 +2,6 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.cli;
 
-import kala.collection.Seq;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.ImmutableSet;
@@ -18,7 +17,6 @@
 import org.junit.jupiter.api.Test;
 
 import java.nio.file.Path;
-import java.util.Arrays;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
 
@@ -71,7 +69,7 @@ public void addModulePath(@NotNull Path newPath) {
    * Create a {@link LibraryConfig} for identifying.
    */
   private @NotNull LibraryConfig config(@NotNull String name) {
-    var libRoot = Path.of("/home/senpai/" + name);
+    var libRoot = Path.of(STR."/home/senpai/\{name}");
 
     return new LibraryConfig(
       Version.create("11.4.514"),
diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml
index e374082a1..b2f17608f 100644
--- a/gradle/libs.versions.toml
+++ b/gradle/libs.versions.toml
@@ -2,7 +2,7 @@
 # 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"
+project = "0.29.4"
 
 # https://openjdk.org/
 java = "21"
diff --git a/ide-lsp/src/test/java/org/aya/lsp/LspTest.java b/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
index 94eadbc72..7a2985d22 100644
--- a/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
+++ b/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
@@ -37,19 +37,19 @@ public class LspTest {
   }
 
   @Test public void testJustLoad() {
-    launch(TEST_LIB).execute(compile((a, e) -> {}));
+    launch(TEST_LIB).execute(compile((_, _) -> {}));
   }
 
   @Test public void testIncremental() {
     launch(TEST_LIB).execute(
-      compile((a, e) -> {}),
+      compile((_, _) -> {}),
       mutate("StringPrims"),
       compile((a, e) -> assertRemake(a, e, "StringPrims", "HelloWorld"))
     );
   }
 
   @Test public void test541() {
-    launch(TEST_LIB).execute(compile((a, e) -> {
+    launch(TEST_LIB).execute(compile((a, _) -> {
       var testOpt = a.lastCompiled()
         .filter(x -> x.moduleName().getLast().equals("Vec"))
         .flatMap(x -> x.program().get())
@@ -70,7 +70,7 @@ public class LspTest {
 
   @Test public void testRealWorldLike() {
     launch(TEST_LIB).execute(
-      compile((a, e) -> {}),
+      compile((_, _) -> {}),
       mutate("HelloWorld"),
       compile((a, e) -> assertRemake(a, e, "HelloWorld")),
       mutate("NatCore"),
@@ -87,7 +87,7 @@ public void colorful() {
 
     var client = new LspTestClient(initParams);
     client.registerLibrary(TEST_LIB);
-    client.execute(compile((a, e) -> {}));
+    client.execute(compile((_, _) -> {}));
 
     var param = new TextDocumentPositionParams(new TextDocumentIdentifier(
       TEST_LIB.resolve("src").resolve("NatCore.aya").toUri()),
@@ -96,17 +96,17 @@ public void colorful() {
 
     var result0 = client.service.hover(param);
     assertTrue(result0.isPresent());
-    assertEquals("<a href=\"#NatCore-Nat\"><span style=\"color:#218c21;\">Nat</span></a>", result0.get().contents.get(0).value);
+    assertEquals("<a href=\"#NatCore-Nat\"><span style=\"color:#218c21;\">Nat</span></a>", result0.get().contents.getFirst().value);
 
     client.service.updateServerOptions(new ServerOptions(new ServerRenderOptions("IntelliJ", null, RenderOptions.OutputTarget.HTML)));
 
     var result1 = client.service.hover(param);
     assertTrue(result1.isPresent());
-    assertEquals("<a href=\"#NatCore-Nat\"><span style=\"color:#000000;\">Nat</span></a>", result1.get().contents.get(0).value);
+    assertEquals("<a href=\"#NatCore-Nat\"><span style=\"color:#000000;\">Nat</span></a>", result1.get().contents.getFirst().value);
   }
 
   private void logTime(long time) {
-    System.out.println("Remake changed modules took: " + time + "ms");
+    System.out.println(STR."Remake changed modules took: \{time}ms");
   }
 
   private void assertRemake(@NotNull LspTestCompilerAdvisor advisor, long time, @NotNull String... modules) {
diff --git a/pretty/src/main/java/org/aya/pretty/backend/html/DocHtmlPrinter.java b/pretty/src/main/java/org/aya/pretty/backend/html/DocHtmlPrinter.java
index 58fd86b30..d39b144c5 100644
--- a/pretty/src/main/java/org/aya/pretty/backend/html/DocHtmlPrinter.java
+++ b/pretty/src/main/java/org/aya/pretty/backend/html/DocHtmlPrinter.java
@@ -71,7 +71,7 @@ protected void renderCssStyle(@NotNull Cursor cursor) {
     var colors = Html5Stylist.colorsToCss(config.getStylist().colorScheme);
     cursor.invisibleContent("\n:root {\n%s\n}\n".formatted(colors));
     config.getStylist().styleFamily.definedStyles().forEach((name, style) -> {
-      var selector = Html5Stylist.styleKeyToCss(name).map(x -> "." + x).joinToString(" ");
+      var selector = Html5Stylist.styleKeyToCss(name).map(x -> STR.".\{x}").joinToString(" ");
       var css = style.styles().mapNotNull(Html5Stylist::styleToCss).joinToString("\n", "  %s"::formatted);
       var stylesheet = "%s {\n%s\n}\n".formatted(selector, css);
       cursor.invisibleContent(stylesheet);
@@ -107,10 +107,10 @@ protected void renderCssStyle(@NotNull Cursor cursor) {
   protected void renderHyperLinked(@NotNull Cursor cursor, Doc.@NotNull HyperLinked text, EnumSet<Outer> outer) {
     var href = text.href();
     cursor.invisibleContent("<a ");
-    if (text.id() != null) cursor.invisibleContent("id=\"" + normalizeId(text.id()) + "\" ");
+    if (text.id() != null) cursor.invisibleContent(STR."id=\"\{normalizeId(text.id())}\" ");
     if (text.hover() != null) {
       cursor.invisibleContent("class=\"aya-hover\" ");
-      cursor.invisibleContent("aya-hover-text=\"" + text.hover() + "\" ");
+      cursor.invisibleContent(STR."aya-hover-text=\"\{text.hover()}\" ");
     }
     cursor.invisibleContent("href=\"");
     cursor.invisibleContent(normalizeHref(href));
@@ -121,7 +121,7 @@ protected void renderHyperLinked(@NotNull Cursor cursor, Doc.@NotNull HyperLinke
 
   @Override protected void renderImage(@NotNull Cursor cursor, Doc.@NotNull Image image, EnumSet<Outer> outer) {
     cursor.invisibleContent("<img ");
-    cursor.invisibleContent("src=\"" + normalizeHref(image.src()) + "\" ");
+    cursor.invisibleContent(STR."src=\"\{normalizeHref(image.src())}\" ");
     cursor.invisibleContent("alt=\"");
     renderDoc(cursor, image.alt(), outer);
     cursor.invisibleContent("\"/>");
@@ -134,10 +134,10 @@ protected void renderHyperLinked(@NotNull Cursor cursor, Doc.@NotNull HyperLinke
         var prefix = config.opt(StringPrinterConfig.LinkOptions.CrossLinkPrefix, "/");
         var postfix = config.opt(StringPrinterConfig.LinkOptions.CrossLinkPostfix, ".html");
         var sep = config.opt(StringPrinterConfig.LinkOptions.CrossLinkSeparator, "/");
-        yield path.joinToString(sep, prefix, postfix) + (loc == null ? "" : "#" + normalizeId(loc));
+        yield path.joinToString(sep, prefix, postfix) + (loc == null ? "" : STR."#\{normalizeId(loc)}");
       }
       case Link.DirectLink(var link) -> link;
-      case Link.LocalId(var id) -> id.fold(Html5Stylist::normalizeCssId, x -> "v" + x);
+      case Link.LocalId(var id) -> id.fold(Html5Stylist::normalizeCssId, x -> STR."v\{x}");
       // ^ CSS3 selector does not support IDs starting with a digit, so we prefix them with "v".
       // See https://stackoverflow.com/a/37271406/9506898 for more details.
     };
@@ -147,7 +147,7 @@ protected void renderHyperLinked(@NotNull Cursor cursor, Doc.@NotNull HyperLinke
     return switch (linkId) {
       case Link.CrossLink link -> normalizeId(link);
       case Link.DirectLink(var link) -> link;
-      case Link.LocalId localId -> "#" + normalizeId(localId);
+      case Link.LocalId localId -> STR."#\{normalizeId(localId)}";
     };
   }
 
@@ -159,13 +159,13 @@ protected void renderHyperLinked(@NotNull Cursor cursor, Doc.@NotNull HyperLinke
   protected void renderInlineCode(@NotNull Cursor cursor, Doc.@NotNull InlineCode code, EnumSet<Outer> outer) {
     // `<code class="" />` is valid, see:
     // https://stackoverflow.com/questions/30748847/is-an-empty-class-attribute-valid-html
-    cursor.invisibleContent("<code class=\"" + capitalize(code.language()) + "\">");
+    cursor.invisibleContent(STR."<code class=\"\{capitalize(code.language())}\">");
     renderDoc(cursor, code.code(), EnumSet.of(Outer.EnclosingTag)); // Even in code mode, we still need to escape
     cursor.invisibleContent("</code>");
   }
 
   @Override protected void renderCodeBlock(@NotNull Cursor cursor, Doc.@NotNull CodeBlock block, EnumSet<Outer> outer) {
-    cursor.invisibleContent("<pre class=\"" + capitalize(block.language()) + "\">");
+    cursor.invisibleContent(STR."<pre class=\"\{capitalize(block.language())}\">");
     renderDoc(cursor, block.code(), EnumSet.of(Outer.EnclosingTag)); // Even in code mode, we still need to escape
     cursor.invisibleContent("</pre>");
   }
@@ -186,13 +186,13 @@ protected void renderInlineMath(@NotNull Cursor cursor, Doc.@NotNull InlineMath
   @Override
   protected void renderList(@NotNull Cursor cursor, Doc.@NotNull List list, EnumSet<Outer> outer) {
     var tag = list.isOrdered() ? "ol" : "ul";
-    cursor.invisibleContent("<" + tag + ">");
+    cursor.invisibleContent(STR."<\{tag}>");
     list.items().forEach(item -> {
       cursor.invisibleContent("<li>");
       renderDoc(cursor, item, EnumSet.of(Outer.List, Outer.EnclosingTag));
       cursor.invisibleContent("</li>");
     });
-    cursor.invisibleContent("</" + tag + ">");
+    cursor.invisibleContent(STR."</\{tag}>");
   }
 
   private @NotNull String capitalize(@NotNull org.aya.pretty.doc.Language s) {
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 3fd862e51..8ba5d8408 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
@@ -103,7 +103,7 @@ public ClassedPreset(@NotNull ClosingStylist delegate) {
   }
 
   public static @NotNull String cssVar(@NotNull String name) {
-    return "--" + normalizeCssId(name);
+    return STR."--\{normalizeCssId(name)}";
   }
 
   public static @NotNull String cssColor(int rgb) {
diff --git a/tools-kala/src/main/java/org/aya/util/terck/Relation.java b/tools-kala/src/main/java/org/aya/util/terck/Relation.java
index 98a4cfe3f..90ec1524a 100644
--- a/tools-kala/src/main/java/org/aya/util/terck/Relation.java
+++ b/tools-kala/src/main/java/org/aya/util/terck/Relation.java
@@ -34,7 +34,7 @@ record Decrease(boolean usable, int size) implements Relation {
   @Override default @NotNull Doc toDoc() {
     return switch (this) {
       case Decrease d when d.size == 0 -> Doc.plain("  =");
-      case Decrease d -> Doc.plain((d.usable ? " " : "!") + "-" + d.size);
+      case Decrease d -> Doc.plain(STR."\{d.usable ? " " : "!"}-\{d.size}");
       case Unknown ignored -> Doc.plain("  ?");
     };
   }
diff --git a/tools-repl/src/main/java/org/aya/repl/CommandManager.java b/tools-repl/src/main/java/org/aya/repl/CommandManager.java
index 20487836b..14a41ea7c 100644
--- a/tools-repl/src/main/java/org/aya/repl/CommandManager.java
+++ b/tools-repl/src/main/java/org/aya/repl/CommandManager.java
@@ -43,7 +43,7 @@ public CommandManager(
   private @NotNull CommandGen genCommand(@NotNull Command c) {
     var entry = Seq.of(c.getClass().getDeclaredMethods())
       .findFirst(method -> method.isAnnotationPresent(Command.Entry.class));
-    if (entry.isEmpty()) throw new IllegalArgumentException("no entry found in " + c.getClass());
+    if (entry.isEmpty()) throw new IllegalArgumentException(STR."no entry found in \{c.getClass()}");
     try {
       var method = entry.get();
       method.setAccessible(true); // for anonymous class
@@ -56,10 +56,10 @@ public CommandManager(
       if (param.size() == 2) return new CommandGen(c, handle, null);
       // TODO: support more than 1 parameter
       var factory = argFactory.getOption(param.get(2));
-      if (factory.isEmpty()) throw new IllegalArgumentException("no argument factory found for " + param.get(2));
+      if (factory.isEmpty()) throw new IllegalArgumentException(STR."no argument factory found for \{param.get(2)}");
       return new CommandGen(c, handle, factory.get());
     } catch (IllegalAccessException e) {
-      throw new IllegalArgumentException("unable to unreflect entry for: " + c.names(), e);
+      throw new IllegalArgumentException(STR."unable to unreflect entry for: \{c.names()}", e);
     }
   }
 
@@ -71,7 +71,7 @@ public record Clue(
     public Command.Result run(@NotNull Object repl) throws Throwable {
       return switch (command.size()) {
         case 1 -> command.getFirst().invoke(repl, argument);
-        case 0 -> Command.Result.err("Command `" + name + "` not found", true);
+        case 0 -> Command.Result.err(STR."Command `\{name}` not found", true);
         default -> Command.Result.err(command.view()
             .flatMap(s -> s.owner.names())
             .joinToString("`, `", "Ambiguous command name (`", "`), please be more accurate", s -> s),
diff --git a/tools-repl/src/main/java/org/aya/repl/ReplUtil.java b/tools-repl/src/main/java/org/aya/repl/ReplUtil.java
index b9b4c85f0..aab968c5d 100644
--- a/tools-repl/src/main/java/org/aya/repl/ReplUtil.java
+++ b/tools-repl/src/main/java/org/aya/repl/ReplUtil.java
@@ -16,7 +16,7 @@ public interface ReplUtil {
       return commandManager.cmd.find(c -> c.owner().names().contains(argument.cmd))
         .getOrElse(
           it -> Command.Result.ok(it.owner().help(), true),
-          () -> Command.Result.err("No such command: " + argument.cmd, true));
+          () -> Command.Result.err(STR."No such command: \{argument.cmd}", true));
     }
     var commands = Doc.vcat(commandManager.cmd.view()
       .map(command -> Doc.sep(
diff --git a/tools/src/main/java/org/aya/util/Version.java b/tools/src/main/java/org/aya/util/Version.java
index 0912ef1c8..e9425dc8a 100644
--- a/tools/src/main/java/org/aya/util/Version.java
+++ b/tools/src/main/java/org/aya/util/Version.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;
 
@@ -24,7 +24,7 @@ public record Version(
     if (version.endsWith("-SNAPSHOT")) version = version.substring(0, version.length() - "-SNAPSHOT".length());
     var split = DOT.split(version.trim());
     return switch (split.length) {
-      case 0 -> throw new IllegalArgumentException("Invalid version: " + version);
+      case 0 -> throw new IllegalArgumentException(STR."Invalid version: \{version}");
       case 1 -> new Version(new BigInteger(split[0]), BigInteger.ZERO, BigInteger.ZERO);
       case 2 -> new Version(new BigInteger(split[0]), new BigInteger(split[1]), BigInteger.ZERO);
       default -> new Version(new BigInteger(split[0]), new BigInteger(split[1]), new BigInteger(split[2]));
@@ -41,15 +41,15 @@ public Version(long major, long minor, long patch) {
 
   @Contract(pure = true)
   public @NotNull String getLongString() {
-    return major + "." + minor + "." + patch;
+    return STR."\{major}.\{minor}.\{patch}";
   }
 
   @Override public String toString() {
     return BigInteger.ZERO.equals(patch)
       ? BigInteger.ZERO.equals(minor)
       ? major.toString()
-      : major + "." + minor
-      : major + "." + minor + "." + patch;
+      : STR."\{major}.\{minor}"
+      : STR."\{major}.\{minor}.\{patch}";
   }
 
   @Override public int compareTo(Version o) {
diff --git a/tools/src/main/java/org/aya/util/error/SourcePos.java b/tools/src/main/java/org/aya/util/error/SourcePos.java
index bb23dec41..de64906fd 100644
--- a/tools/src/main/java/org/aya/util/error/SourcePos.java
+++ b/tools/src/main/java/org/aya/util/error/SourcePos.java
@@ -17,7 +17,6 @@
  * @param tokenStartIndex The index of first character (inclusive)
  * @author kiva
  */
-@SuppressWarnings("unused")
 public record SourcePos(
   @NotNull SourceFile file,
   int tokenStartIndex,
@@ -136,8 +135,7 @@ public int linesOfCode() {
   }
 
   @Override public String toString() {
-    return "(" + tokenStartIndex + "-" + tokenEndIndex + ") ["
-      + startLine + "," + startColumn + "-" + endLine + "," + endColumn + ']';
+    return STR."(\{tokenStartIndex}-\{tokenEndIndex}) [\{startLine},\{startColumn}-\{endLine},\{endColumn}\{']'}";
   }
 
   @Override