diff --git a/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java b/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java
index af5b39bfd1..8617d6f555 100644
--- a/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java
+++ b/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java
@@ -1,7 +1,11 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.cli.repl;
 
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
 import kala.control.Either;
@@ -13,6 +17,7 @@
 import org.aya.repl.Command;
 import org.aya.repl.CommandArg;
 import org.aya.repl.ReplUtil;
+import org.aya.syntax.compile.JitDef;
 import org.aya.syntax.core.def.AnyDef;
 import org.aya.syntax.core.def.ConDefLike;
 import org.aya.syntax.core.def.MemberDefLike;
@@ -22,10 +27,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.io.IOException;
-import java.nio.file.Files;
-import java.nio.file.Path;
-
 public interface ReplCommands {
   record Code(@NotNull String code) { }
   record Prompt(@NotNull String prompt) { }
@@ -65,10 +66,11 @@ record StyleParam(@NotNull Either<RenderOptions.StyleFamilyName, Path> value)
         default -> {
         }
       }
-      if (topLevel instanceof TyckAnyDef<?> tyckDef) {
-        return new Command.Result(Output.stdout(repl.render(tyckDef.core())), true);
-      }
-      return Command.Result.ok(topLevel.name(), true);      // TODO: pretty print
+
+      return new Result(Output.stdout((switch (topLevel) {
+        case JitDef jitDef -> repl.render(jitDef);
+        case TyckAnyDef<?> tyckDef -> repl.render(tyckDef.core());
+      })), true);
     }
   };
 
@@ -82,7 +84,7 @@ record StyleParam(@NotNull Either<RenderOptions.StyleFamilyName, Path> value)
   @NotNull Command SHOW_SHAPES = new Command(ImmutableSeq.of("debug-show-shapes"), "Show recognized shapes") {
     @Entry public @NotNull Command.Result execute(@NotNull AyaRepl repl) {
       var discovered = repl.replCompiler.getShapeFactory().discovered;
-      return Result.ok(repl.renderDoc(Doc.vcat(discovered.mapTo(MutableList.create(),
+      return new Result(Output.stdout(Doc.vcat(discovered.mapTo(MutableList.create(),
         (def, recog) ->
           Doc.sep(BasePrettier.refVar(def),
             Doc.symbol("=>"),
@@ -98,7 +100,7 @@ record StyleParam(@NotNull Either<RenderOptions.StyleFamilyName, Path> value)
         return Result.err("Unable to load file or library: " + e.getLocalizedMessage(), true);
       }
       // SingleFileCompiler would print result to REPL.
-      return new Result(Output.empty(), true);
+      return new Result(Output.EMPTY, true);
     }
   };
 
@@ -118,7 +120,7 @@ record StyleParam(@NotNull Either<RenderOptions.StyleFamilyName, Path> value)
       repl.cwd = path;
       // for jline completer to work properly, but it does not have any effect actually
       System.setProperty("user.dir", path.toAbsolutePath().toString());
-      return new Result(Output.empty(), true);
+      return new Result(Output.EMPTY, true);
     }
   };
 
diff --git a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
index 1778a195bc..4cd32a4477 100644
--- a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
+++ b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
@@ -1,7 +1,12 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.test.cli;
 
+import java.io.IOException;
+import java.nio.file.Paths;
+
+import static org.junit.jupiter.api.Assertions.*;
+
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.cli.interactive.ReplCompiler;
 import org.aya.generic.Constants;
@@ -14,7 +19,9 @@
 import org.aya.syntax.core.term.repr.IntegerTerm;
 import org.aya.syntax.literate.CodeOptions.NormalizeMode;
 import org.aya.syntax.ref.AnyVar;
+import org.aya.syntax.ref.CompiledVar;
 import org.aya.syntax.ref.DefVar;
+import org.aya.util.error.Global;
 import org.aya.util.error.SourcePos;
 import org.aya.util.reporter.ThrowingReporter;
 import org.jetbrains.annotations.NotNull;
@@ -22,25 +29,40 @@
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 
-import java.io.IOException;
-import java.nio.file.Paths;
-
-import static org.junit.jupiter.api.Assertions.*;
-
 public class ReplCompilerTest {
   public final @NotNull ReplCompiler compiler = new ReplCompiler(ImmutableSeq.empty(), new ThrowingReporter(AyaPrettierOptions.debug()), null);
 
   @BeforeEach public void setup() {
     compiler.getContext().clear();
     compiler.imports.clear();
+    Global.NO_RANDOM_NAME = true;
   }
 
   @Test public void library() throws IOException {
     compiler.loadToContext(Paths.get("../ide-lsp", "src", "test", "resources", "lsp-test-lib"));
-    assertNotNull(findContext("Nat::Core::zero"));
-    assertNotNull(findContext("VecCore::vnil"));
     assertNotNull(findContext("VecCore:::>"));
 
+    var vnil = assertInstanceOf(CompiledVar.class, findContext("VecCore::vnil"));
+    assertNotNull(vnil);
+    assertEquals("| /* compiled pattern */ => vnil", vnil.core().easyToString());
+
+    var zero = assertInstanceOf(CompiledVar.class, findContext("Nat::Core::zero"));
+    assertNotNull(zero);
+    assertEquals("| zero", zero.core().easyToString());
+
+    var Nat = assertInstanceOf(CompiledVar.class, findContext("Nat::Core::Nat"));
+    assertNotNull(Nat);
+    assertEquals("""
+      inductive Nat : Type 0
+        | zero
+        | suc (_ : Nat)
+      """.trim(), Nat.core().easyToString());
+
+    var refl = assertInstanceOf(CompiledVar.class, findContext("Path::refl"));
+    assertNotNull(refl);
+    assertEquals("def refl {A : Type 0} {a : A} : a = a => /* compiled code */",
+      refl.core().easyToString());
+
     // Don't be too harsh on the test lib structure, maybe we will change it
     var rootHints = compiler.getContext().giveMeHint(ImmutableSeq.empty());
     assertTrue(rootHints.contains("Nat"));
diff --git a/cli-impl/src/test/resources/negative/PatCohError.txt b/cli-impl/src/test/resources/negative/PatCohError.txt
index 5de67a76d7..9ce9df5caf 100644
--- a/cli-impl/src/test/resources/negative/PatCohError.txt
+++ b/cli-impl/src/test/resources/negative/PatCohError.txt
@@ -9,7 +9,7 @@ In file $FILE:10:0 ->
      │ ╰─────────────────╯
 
 Error: I'm unsure if there should be a case for constructor
-         | suc m ⇒ fsuc (_ : Fin+1 ^0)
+         | suc m ⇒ fsuc (_ : Fin+1 m)
        because I got stuck on the index unification of type
          Fin+1 m
 
diff --git a/syntax/src/main/java/org/aya/prettier/BasePrettier.java b/syntax/src/main/java/org/aya/prettier/BasePrettier.java
index 36bc7a18be..80cfec1dbc 100644
--- a/syntax/src/main/java/org/aya/prettier/BasePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/BasePrettier.java
@@ -1,7 +1,13 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.prettier;
 
+import java.util.Objects;
+import java.util.function.BiFunction;
+import java.util.function.ToIntBiFunction;
+
+import static org.aya.prettier.Tokens.KW_PRIM;
+
 import kala.collection.Seq;
 import kala.collection.SeqLike;
 import kala.collection.SeqView;
@@ -30,12 +36,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.Objects;
-import java.util.function.BiFunction;
-import java.util.function.ToIntBiFunction;
-
-import static org.aya.prettier.Tokens.KW_PRIM;
-
 public abstract class BasePrettier<Term extends AyaDocile> {
   public static @NotNull Doc coreArgsDoc(@NotNull PrettierOptions options, @NotNull SeqView<? extends AyaDocile> self) {
     return Doc.commaList(self.map(t -> t.toDoc(options)));
@@ -191,11 +191,9 @@ protected static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull Bin
         ? Doc.parened(withEx) : withEx;
   }
 
-  /**
-   * Pretty-print a telescope in a dumb (but conservative) way.
-   *
-   * @see #visitTele(Seq, AyaDocile, Usage)
-   */
+  /// Pretty-print a telescope in a dumb (but conservative) way.
+  ///
+  /// @see #visitTele(Seq, AyaDocile, Usage)
   public @NotNull Doc visitTele(@NotNull Seq<? extends ParamLike<Term>> telescope) {
     return visitTele(telescope, null, (_, _) -> 1);
   }
@@ -211,7 +209,7 @@ protected static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull Bin
    * @param altF7 a function for finding usages.
    * @see #visitTele(Seq)
    */
-  public @NotNull Doc visitTele(
+  public final @NotNull Doc visitTele(
     @NotNull Seq<? extends ParamLike<Term>> telescope,
     @Nullable Term body, @NotNull Usage<Term, LocalVar> altF7
   ) {
@@ -256,8 +254,7 @@ protected static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull Bin
 
   private Doc mutableListNames(MutableList<? extends ParamLike<?>> names, ParamLike<?> param) {
     // We HAVE TO collect the results, since {names} is mutable, therefore {names.view()} becomes mutable.
-    var namesDocs = names.view().map(ParamLike::nameDoc)
-      .toImmutableSeq();
+    var namesDocs = names.map(ParamLike::nameDoc);
     return param.toDoc(Doc.sep(namesDocs), options);
   }
 
@@ -281,7 +278,7 @@ protected boolean optionImplicit() {
     return coerce ? Doc.styled(KEYWORD, "coerce") : Doc.empty();
   }
 
-  static @NotNull Doc primDoc(DefVar<?, ?> ref) {
+  static @NotNull Doc primDoc(AnyDefVar ref) {
     return Doc.sep(KW_PRIM, refVar(ref));
   }
 
diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index b3d4b81664..7eea4c54cf 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -2,23 +2,28 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.prettier;
 
+import java.util.EnumSet;
+import java.util.function.BiFunction;
 import java.util.function.Function;
 import java.util.function.UnaryOperator;
 
 import static org.aya.prettier.Tokens.*;
 
 import com.intellij.openapi.util.text.StringUtil;
-import kala.collection.SeqLike;
+import kala.collection.Seq;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.FreezableMutableList;
 import kala.collection.mutable.MutableList;
 import kala.control.Either;
+import kala.value.LazyValue;
 import org.aya.generic.AyaDocile;
+import org.aya.generic.Modifier;
 import org.aya.generic.Renamer;
 import org.aya.generic.term.DTKind;
 import org.aya.generic.term.ParamLike;
 import org.aya.pretty.doc.Doc;
-import org.aya.syntax.compile.JitMatchy;
+import org.aya.syntax.compile.*;
 import org.aya.syntax.concrete.stmt.decl.DataCon;
 import org.aya.syntax.core.RichParam;
 import org.aya.syntax.core.def.*;
@@ -31,9 +36,11 @@
 import org.aya.syntax.core.term.repr.MetaLitTerm;
 import org.aya.syntax.core.term.repr.StringTerm;
 import org.aya.syntax.core.term.xtt.*;
+import org.aya.syntax.ref.CompiledVar;
 import org.aya.syntax.ref.DefVar;
 import org.aya.syntax.ref.GenerateKind.Basic;
 import org.aya.syntax.ref.LocalVar;
+import org.aya.syntax.telescope.AbstractTele;
 import org.aya.util.Arg;
 import org.aya.util.error.SourcePos;
 import org.aya.util.prettier.PrettierOptions;
@@ -56,10 +63,9 @@ public class CorePrettier extends BasePrettier<Term> {
     return switch (preterm) {
       case FreeTerm(var var) -> varDoc(var);
       case LocalTerm(var idx) -> Doc.plain("^" + idx);
-      case MetaCall term -> {
-        var name = term.ref();
+      case MetaCall(var name, var args) -> {
         var inner = Doc.cat(Doc.plain("?"), varDoc(name));
-        Function<Outer, Doc> factory = o -> visitCoreApp(null, inner, term.args().view(), o, optionImplicit());
+        Function<Outer, Doc> factory = o -> visitCoreApp(null, inner, args.view(), o, optionImplicit());
         if (options.map.get(AyaPrettierOptions.Key.InlineMetas)) yield factory.apply(outer);
         yield Doc.wrap(HOLE_LEFT, HOLE_RIGHT, factory.apply(Outer.Free));
       }
@@ -73,10 +79,8 @@ public class CorePrettier extends BasePrettier<Term> {
       case IntegerTerm shaped -> shaped.repr() == 0
         ? linkLit(0, shaped.zero(), CON)
         : linkLit(shaped.repr(), shaped.suc(), CON);
-      case ListTerm shaped -> {
-        var subterms = shaped.repr().map(x -> term(Outer.Free, x));
-        var nil = shaped.nil();
-        var cons = shaped.cons();
+      case ListTerm(var repr, var nil, var cons, _) -> {
+        var subterms = repr.map(x -> term(Outer.Free, x));
         yield Doc.sep(
           linkListLit(Doc.symbol("["), nil, CON),
           Doc.join(linkListLit(Doc.COMMA, cons, CON), subterms),
@@ -237,8 +241,7 @@ private ImmutableSeq<Term> visibleArgsOf(Callable call) {
   }
 
   private @NotNull Doc visitAccessHead(@NotNull MemberCall term) {
-    return Doc.cat(term(Outer.ProjHead, term.of()), Doc.symbol("."),
-      refVar(term.ref()));
+    return Doc.cat(term(Outer.ProjHead, term.of()), Doc.symbol("."), refVar(term.ref()));
   }
 
   public @NotNull Doc pat(@NotNull Pat pat, boolean licit, Outer outer) {
@@ -271,107 +274,173 @@ private ImmutableSeq<Term> visibleArgsOf(Callable call) {
     return switch (predef) {
       case PrimDef def -> primDoc(def.ref());
       case FnDef def -> {
-        var line1 = MutableList.of(KW_DEF);
-        def.modifiers().forEach(m -> line1.append(Doc.styled(KEYWORD, m.keyword)));
-        var tele = enrich(def.telescope());
-        var subst = tele.view().<Term>map(p -> new FreeTerm(p.ref()));
-        line1.appendAll(new Doc[]{
-          defVar(def.ref()),
-          visitTele(tele),
-          HAS_TYPE,
-          term(Outer.Free, def.result().instTeleVar(tele.view().map(ParamLike::ref)))
-        });
-        var line1sep = Doc.sepNonEmpty(line1);
-        yield switch (def.body()) {
-          case Either.Left(var term) -> Doc.sep(line1sep, FN_DEFINED_AS, term(Outer.Free, term.instTele(subst)));
-          case Either.Right(var body) -> Doc.vcat(line1sep,
-            Doc.nest(2, visitClauses(body.matchingsView(), tele.view().map(ParamLike::explicit))));
-        };
+        var absTele = TyckDef.defSignature(def);
+        yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
+          (prefix, subst) -> switch (def.body()) {
+            case Either.Left(var term) -> Doc.sep(prefix, FN_DEFINED_AS, term(Outer.Free, term.instTele(subst.view())));
+            case Either.Right(var body) -> Doc.vcat(prefix,
+              Doc.nest(2, visitClauses(body.matchingsView(), def.telescope().view().map(Param::explicit))));
+          });
       }
-      case MemberDef field -> Doc.sepNonEmpty(Doc.symbol("|"),
-        defVar(field.ref()),
-        visitTele(enrich(field.telescope())),
-        Doc.symbol(":"),
-        term(Outer.Free, field.result()));
-      case ConDef con -> {
-        var doc = Doc.sepNonEmpty(coe(con.coerce),
-          defVar(con.ref()),
-          visitTele(enrich(con.selfTele)));
-        if (con.pats.isNotEmpty()) {
-          var pats = Doc.commaList(con.pats.view().map(pat -> pat(pat, true, Outer.Free)));
-          yield Doc.sep(Doc.symbol("|"), pats, Doc.symbol("=>"), doc);
-        } else {
-          yield Doc.sep(BAR, doc);
+      case MemberDef field -> visitMember(defVar(field.ref()), TyckDef.defSignature(field));
+      case ConDef con -> visitCon(con.ref, con.coerce, con.selfTele);
+      case ClassDef def -> visitClass(defVar(def.ref()), def.members().view().map(this::def));
+      case DataDef def -> visitData(new DataDef.Delegate(def.ref()));
+    };
+  }
+
+  public @NotNull Doc def(@NotNull AnyDef unit) {
+    return switch (unit) {
+      case JitDef jitDef -> def(jitDef);
+      case TyckAnyDef<?> tyckAnyDef -> def(tyckAnyDef.ref.core);
+    };
+  }
+
+  @Override public @NotNull Doc visitTele(@NotNull Seq<? extends ParamLike<Term>> telescope) {
+    return visitTele(telescope, null, FindUsage::free);
+  }
+
+  public @NotNull Doc def(@NotNull JitDef unit) {
+    var dummyVar = new CompiledVar(unit);
+    var nameDoc = defVar(dummyVar);
+
+    return switch (unit) {
+      case JitFn jitFn -> visitFn(nameDoc, jitFn.modifiers(), jitFn, (prefix, _) ->
+        Doc.sep(prefix, FN_DEFINED_AS, COMMENT_COMPILED_CODE));
+      case JitCon jitCon -> {
+        var dummyOwnerArgs = ImmutableSeq.<Term>fill(jitCon.ownerTeleSize(), i -> new FreeTerm(jitCon.telescopeName(i)));
+        var rhs = visitConRhs(nameDoc, false, jitCon.inst(dummyOwnerArgs));
+        var wholeClause = rhs;
+
+        if (jitCon.dataRef().signature().telescopeSize() > 0) {
+          // may have pattern, but we don't know!
+          wholeClause = Doc.sep(COMMENT_COMPILED_PATTERN, FN_DEFINED_AS, rhs);
         }
+
+        yield Doc.sep(BAR, wholeClause);
       }
-      case ClassDef def -> Doc.vcat(Doc.sepNonEmpty(KW_CLASS,
-        defVar(def.ref()),
-        Doc.nest(2, Doc.vcat(def.members().view().map(this::def)))));
-      case DataDef def -> {
-        var richDataTele = enrich(def.telescope());
-        var dataArgs = richDataTele.view().<Term>map(t -> new FreeTerm(t.ref()));
-
-        var line1 = MutableList.of(KW_DATA,
-          defVar(def.ref()),
-          visitTele(richDataTele),
-          HAS_TYPE,
-          term(Outer.Free, def.result()));
-        var cons = def.body.view().map(con ->
-          // we need to instantiate the tele of con, but we can't modify the CtorDef
-          visitCon(con.ref, enrich(con.selfTele.mapIndexed((i, p) -> {
-            // i: nth param
-            // p: the param
-            // instantiate reference to data tele
-            return p.descent(t -> t.instTeleFrom(i, dataArgs));
-          })), con.coerce));
-
-        yield Doc.vcat(Doc.sepNonEmpty(line1),
-          Doc.nest(2, Doc.vcat(cons)));
-      }
+      case JitData jitData -> visitData(jitData);
+      case JitMember jitMember -> visitMember(nameDoc, jitMember);
+      case JitClass jitClass -> visitClass(nameDoc, jitClass.members().view().map(this::def));
+      case JitPrim _ -> primDoc(dummyVar);
     };
   }
 
+  private @NotNull Doc visitFn(
+    @NotNull Doc name,
+    @NotNull EnumSet<Modifier> modifiers,
+    @NotNull AbstractTele telescope,
+    @NotNull BiFunction<Doc, ImmutableSeq<Term>, Doc> cont
+  ) {
+    var line1 = MutableList.of(KW_DEF);
+    modifiers.forEach(m -> line1.append(Doc.styled(KEYWORD, m.keyword)));
+    line1.append(name);
+
+    var tele = enrich(telescope);
+    line1.append(visitTele(tele));
+    line1.append(HAS_TYPE);
+
+    var subst = tele.<Term>map(x -> new FreeTerm(x.ref()));
+    line1.append(term(Outer.Free, telescope.result(subst)));
+
+    var line1Doc = Doc.sepNonEmpty(line1);
+    return cont.apply(line1Doc, subst);
+  }
+
+  /// @param selfTele self tele of the constructor, unlike [JitCon], the data args/owner args should be supplied.
+  private @NotNull Doc visitConRhs(@NotNull Doc name, boolean coerce, @NotNull AbstractTele selfTele) {
+    return Doc.sepNonEmpty(coe(coerce), name, visitTele(enrich(selfTele)));
+  }
+
   private @NotNull Doc visitCon(
     @NotNull DefVar<ConDef, DataCon> ref,
-    @NotNull ImmutableSeq<ParamLike<Term>> richSelfTele,
-    boolean coerce
+    boolean coerce,
+    @NotNull ImmutableSeq<Param> rawSelfTele
   ) {
-    var doc = Doc.sepNonEmpty(coe(coerce), defVar(ref), visitTele(richSelfTele));
     var con = ref.core;
-    if (con.pats.isNotEmpty()) {
-      var pats = Doc.commaList(con.pats.view().map(pat -> pat(pat, true, Outer.Free)));
-      return Doc.sep(BAR, pats, FN_DEFINED_AS, doc);
+    var conName = defVar(ref);
+    var pats = con.pats;
+
+    if (pats.isNotEmpty()) {
+      var dataSig = con.dataRef.signature();
+      var licits = ImmutableSeq.fill(dataSig.telescopeSize(), dataSig::telescopeLicit).view();
+      return visitClause(pats, licits, ownerArgs -> {
+        var realSelfTele = Param.instTele(rawSelfTele.view(), ownerArgs).toImmutableSeq();
+        return visitConRhs(conName, coerce, new AbstractTele.Locns(realSelfTele, ErrorTerm.DUMMY));
+      });
     } else {
-      return Doc.sep(BAR, doc);
+      var ownerArgs = con.ownerTele.<Term>map(Param::toFreshTerm);
+      var realSelfTele = Param.instTele(rawSelfTele.view(), ownerArgs.view()).toImmutableSeq();
+      return Doc.sep(BAR, visitConRhs(conName, coerce, new AbstractTele.Locns(realSelfTele, ErrorTerm.DUMMY)));
     }
   }
 
-  public @NotNull Doc visitClauseLhs(@NotNull SeqView<Boolean> licits, @NotNull Term.Matching clause) {
-    var enrichPats = clause.patterns().zip(licits,
-      (pat, licit) -> pat(pat, licit, Outer.Free));
+  private @NotNull Doc visitData(@NotNull DataDefLike dataDef) {
+    var name = defVar(AnyDef.toVar(dataDef));
+    var telescope = dataDef.signature();
+    var richDataTele = enrich(telescope);
+    var dataArgs = richDataTele.<Term>map(t -> new FreeTerm(t.ref()));
+
+    var line1 = Doc.sepNonEmpty(KW_DATA, name,
+      visitTele(richDataTele),
+      HAS_TYPE,
+      term(Outer.Free, telescope.result(dataArgs)));
+    var consDoc = dataDef.body().view().map(this::def);
+
+    return Doc.vcat(line1, Doc.nest(2, Doc.vcat(consDoc)));
+  }
+
+  /// @param telescope the telescope of a [MemberDefLike], including the `self` parameter
+  private @NotNull Doc visitMember(@NotNull Doc name, @NotNull AbstractTele telescope) {
+    // TODO: should we pretty print the `self` parameter?
+    //       The use of `self` parameter still appears in other parameters.
+    var visitTele = visitTele(telescope);
+
+    return Doc.sepNonEmpty(BAR, name, visitTele.tele, HAS_TYPE, visitTele.result.get());
+  }
+
+  private @NotNull Doc visitClass(@NotNull Doc name, @NotNull SeqView<Doc> members) {
+    return Doc.sepNonEmpty(KW_CLASS, name, Doc.nest(2, Doc.vcat(members)));
+  }
+
+  public @NotNull Doc visitClauseLhs(@NotNull ImmutableSeq<Pat> patterns, @NotNull SeqView<Boolean> licits) {
+    var enrichPats = patterns.zip(licits, (pat, licit) -> pat(pat, licit, Outer.Free));
     return Doc.commaList(enrichPats);
   }
 
-  private @NotNull Doc visitClause(@NotNull Term.Matching clause, @NotNull SeqView<Boolean> licits) {
-    var patSubst = Pat.collectRichBindings(clause.patterns().view());
-    var lhsWithoutBar = visitClauseLhs(licits, clause);
-    var rhs = term(Outer.Free, clause.body().instTele(patSubst.view().map(RichParam::toTerm)));
+  private @NotNull Doc visitClause(
+    @NotNull ImmutableSeq<Pat> patterns,
+    @NotNull SeqView<Boolean> licits,
+    @NotNull Function<SeqView<Term>, Doc> bodyCont
+  ) {
+    var patSubst = Pat.collectRichBindings(patterns.view());
+    var lhsWithoutBar = visitClauseLhs(patterns, licits);
+    var subst = patSubst.view().<Term>map(RichParam::toTerm);
+    var rhs = bodyCont.apply(subst);
 
     return Doc.sep(BAR, lhsWithoutBar, FN_DEFINED_AS, rhs);
   }
 
+  private @NotNull Doc visitClause(@NotNull Term.Matching clause, @NotNull SeqView<Boolean> licits) {
+    return visitClause(clause.patterns(), licits, subst -> term(Outer.Free, clause.body().instTele(subst)));
+  }
+
   private @NotNull Doc visitClauses(@NotNull SeqView<Term.Matching> clauses, @NotNull SeqView<Boolean> licits) {
     return Doc.vcat(clauses.map(matching -> visitClause(matching, licits)));
   }
 
   // region Name Generation
-  private @NotNull ImmutableSeq<ParamLike<Term>> enrich(@NotNull SeqLike<Param> tele) {
-    var richTele = MutableList.<ParamLike<Term>>create();
+  private @NotNull ImmutableSeq<ParamLike<Term>> enrich(@NotNull AbstractTele tele) {
+    var richTele = FreezableMutableList.<ParamLike<Term>>create();
 
-    for (var param : tele) {
-      var freeTy = param.type().instTeleVar(richTele.view().map(ParamLike::ref));
-      richTele.append(new RichParam(new LocalVar(
-        param.name(), SourcePos.NONE, Basic.Pretty), freeTy, param.explicit()));
+    for (var i = 0; i < tele.telescopeSize(); ++i) {
+      var binds = richTele.<Term>map(x -> new FreeTerm(x.ref()));
+      var type = tele.telescope(i, binds);
+      richTele.append(new RichParam(
+        new LocalVar(tele.telescopeName(i), SourcePos.NONE, Basic.Pretty),
+        type,
+        tele.telescopeLicit(i))
+      );
     }
 
     return richTele.toImmutableSeq();
@@ -380,5 +449,17 @@ yield switch (def.body()) {
   private @NotNull LocalVar generateName(@Nullable Term whty) {
     return nameGen.bindName(whty);
   }
+
+  record VisitTele(@NotNull Doc tele, @NotNull LazyValue<Doc> result) { }
+
+  private @NotNull VisitTele visitTele(@NotNull AbstractTele tele) {
+    var richTele = enrich(tele);
+    var teleDoc = visitTele(richTele);
+
+    return new VisitTele(teleDoc, LazyValue.of(() -> {
+      var binds = richTele.<Term>map(x -> new FreeTerm(x.ref()));
+      return term(Outer.Free, tele.result(binds));
+    }));
+  }
   // endregion Name Generating
 }
diff --git a/syntax/src/main/java/org/aya/prettier/Tokens.java b/syntax/src/main/java/org/aya/prettier/Tokens.java
index ed765fccfc..8a08fce590 100644
--- a/syntax/src/main/java/org/aya/prettier/Tokens.java
+++ b/syntax/src/main/java/org/aya/prettier/Tokens.java
@@ -4,8 +4,7 @@
 
 import org.aya.pretty.doc.Doc;
 
-import static org.aya.prettier.BasePrettier.KEYWORD;
-import static org.aya.prettier.BasePrettier.PRIM;
+import static org.aya.prettier.BasePrettier.*;
 
 public final class Tokens {
 
@@ -52,4 +51,7 @@ private Tokens() {
   public static final Doc KW_IMPORT = Doc.styled(KEYWORD, "import");
   public static final Doc KW_INTERVAL = Doc.styled(PRIM, "I");
   public static final Doc KW_COE = Doc.styled(KEYWORD, "coe");
+
+  public static final Doc COMMENT_COMPILED_CODE = Doc.styled(COMMENT, "/* compiled code */");
+  public static final Doc COMMENT_COMPILED_PATTERN = Doc.styled(COMMENT, "/* compiled pattern */");
 }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitClass.java b/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
index 437266dcdf..cc631c6344 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.syntax.compile;
 
@@ -20,7 +20,7 @@ protected JitClass() {
 
   public abstract @NotNull JitMember[] membars();
 
-  @Override public final @NotNull ImmutableSeq<MemberDefLike> members() {
+  @Override public final @NotNull ImmutableSeq<JitMember> members() {
     return ImmutableArray.Unsafe.wrap(membars());
   }
 
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitData.java b/syntax/src/main/java/org/aya/syntax/compile/JitData.java
index 4d437cc789..a36940d60f 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitData.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitData.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.syntax.compile;
 
@@ -26,7 +26,7 @@ protected JitData(int telescopeSize, boolean[] telescopeLicit, String[] telescop
    * @implNote We should use `constructors()` rather than `constructors`,
    * since `constructors()` will initialize them
    */
-  @Override public @NotNull ImmutableSeq<ConDefLike> body() {
+  @Override public @NotNull ImmutableSeq<JitCon> body() {
     return ImmutableArray.Unsafe.wrap(constructors());
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitDef.java b/syntax/src/main/java/org/aya/syntax/compile/JitDef.java
index d5543978a5..2071ff8809 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitDef.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitDef.java
@@ -1,11 +1,15 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.syntax.compile;
 
+import org.aya.generic.AyaDocile;
+import org.aya.prettier.CorePrettier;
+import org.aya.pretty.doc.Doc;
 import org.aya.syntax.core.def.AnyDef;
 import org.aya.syntax.ref.ModulePath;
 import org.aya.syntax.telescope.JitTele;
 import org.aya.util.binop.Assoc;
+import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -14,7 +18,7 @@
  *
  * @implNote every definition should be annotated by {@link CompiledAya}
  */
-public abstract sealed class JitDef extends JitUnit implements AnyDef permits JitClass, JitTele {
+public abstract sealed class JitDef extends JitUnit implements AnyDef, AyaDocile permits JitClass, JitTele {
   @Override public @NotNull ModulePath fileModule() {
     return new ModulePath(module().module().take(metadata().fileModuleSize()));
   }
@@ -32,4 +36,8 @@ public abstract sealed class JitDef extends JitUnit implements AnyDef permits Ji
   }
 
   @Override public abstract @NotNull JitTele signature();
+
+  @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
+    return new CorePrettier(options).def(this);
+  }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitFn.java b/syntax/src/main/java/org/aya/syntax/compile/JitFn.java
index e261d15a4f..e25147efbc 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitFn.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitFn.java
@@ -1,7 +1,9 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.syntax.compile;
 
+import java.util.EnumSet;
+
 import kala.collection.Seq;
 import org.aya.generic.Modifier;
 import org.aya.syntax.core.def.FnDefLike;
@@ -24,4 +26,10 @@ protected JitFn(int telescopeSize, boolean[] telescopeLicit, String[] telescopeN
   @Override public boolean is(@NotNull Modifier mod) {
     return (modifiers & (1 << mod.ordinal())) != 0;
   }
+
+  public @NotNull EnumSet<Modifier> modifiers() {
+    var set = EnumSet.noneOf(Modifier.class);
+    for (var modi : Modifier.values()) if (is(modi)) set.add(modi);
+    return set;
+  }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java b/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
index fe1705bf3a..1c07866bf0 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.syntax.compile;
 
diff --git a/syntax/src/main/java/org/aya/syntax/core/RichParam.java b/syntax/src/main/java/org/aya/syntax/core/RichParam.java
index 48943b0989..78d97ec54f 100644
--- a/syntax/src/main/java/org/aya/syntax/core/RichParam.java
+++ b/syntax/src/main/java/org/aya/syntax/core/RichParam.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.syntax.core;
 
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/ClassDef.java b/syntax/src/main/java/org/aya/syntax/core/def/ClassDef.java
index c158446ac4..a90b725ec0 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/ClassDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/ClassDef.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.syntax.core.def;
 
@@ -28,10 +28,10 @@ public record ClassDef(
 ) implements TopLevelDef {
   public ClassDef { ref.initialize(this); }
   public static final class Delegate extends TyckAnyDef<ClassDef> implements ClassDefLike {
-    private final @NotNull LazyValue<ImmutableSeq<MemberDefLike>> members = LazyValue.of(() ->
+    private final @NotNull LazyValue<ImmutableSeq<MemberDef.Delegate>> members = LazyValue.of(() ->
       core().members.map(x -> new MemberDef.Delegate(x.ref())));
 
     public Delegate(@NotNull DefVar<ClassDef, ?> ref) { super(ref); }
-    @Override public @NotNull ImmutableSeq<MemberDefLike> members() { return members.get(); }
+    @Override public @NotNull ImmutableSeq<MemberDef.Delegate> members() { return members.get(); }
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
index 644e13e9d9..92243f9581 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.syntax.core.def;
 
@@ -10,7 +10,7 @@
 import org.jetbrains.annotations.NotNull;
 
 public sealed interface ClassDefLike extends AnyDef permits JitClass, ClassDef.Delegate {
-  @NotNull ImmutableSeq<MemberDefLike> members();
+  @NotNull ImmutableSeq<? extends MemberDefLike> members();
 
   default @NotNull Term telescope(int i, @NotNull Seq<Term> restriction) {
     var member = members().get(i);
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/DataDef.java b/syntax/src/main/java/org/aya/syntax/core/def/DataDef.java
index d2e52313f7..87536dfe28 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/DataDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/DataDef.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.syntax.core.def;
 
@@ -28,7 +28,7 @@ public DataDef(@NotNull DefVar<DataDef, DataDecl> ref, @NotNull ImmutableSeq<Con
 
   public static final class Delegate extends TyckAnyDef<DataDef> implements DataDefLike {
     public Delegate(@NotNull DefVar<DataDef, ?> ref) { super(ref); }
-    @Override public @NotNull ImmutableSeq<ConDefLike>
+    @Override public @NotNull ImmutableSeq<ConDef.Delegate>
     body() { return ref.core.body.map(x -> new ConDef.Delegate(x.ref)); }
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/DataDefLike.java b/syntax/src/main/java/org/aya/syntax/core/def/DataDefLike.java
index 1f7595b965..9456ebe5e1 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/DataDefLike.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/DataDefLike.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.syntax.core.def;
 
@@ -7,5 +7,5 @@
 import org.jetbrains.annotations.NotNull;
 
 public sealed interface DataDefLike extends AnyDef permits JitData, DataDef.Delegate {
-  @NotNull ImmutableSeq<ConDefLike> body();
+  @NotNull ImmutableSeq<? extends ConDefLike> body();
 }
diff --git a/tools-repl/src/main/java/org/aya/repl/Command.java b/tools-repl/src/main/java/org/aya/repl/Command.java
index 73adb0b608..eb140dcc8a 100644
--- a/tools-repl/src/main/java/org/aya/repl/Command.java
+++ b/tools-repl/src/main/java/org/aya/repl/Command.java
@@ -1,17 +1,17 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.repl;
 
-import kala.collection.immutable.ImmutableSeq;
-import org.aya.pretty.doc.Doc;
-import org.jetbrains.annotations.NonNls;
-import org.jetbrains.annotations.NotNull;
-
 import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
 
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.pretty.doc.Doc;
+import org.jetbrains.annotations.NonNls;
+import org.jetbrains.annotations.NotNull;
+
 public abstract class Command {
   @Retention(RetentionPolicy.RUNTIME)
   @Target(ElementType.METHOD)
@@ -33,7 +33,7 @@ public Command(@NotNull ImmutableSeq<String> names, @NotNull String help) {
   public final @NotNull String help() { return help; }
 
   public record Output(@NotNull Doc stdout, @NotNull Doc stderr) {
-    public static @NotNull Output empty() { return new Output(Doc.empty(), Doc.empty()); }
+    public static final Output EMPTY = new Output(Doc.empty(), Doc.empty());
     public static @NotNull Output stdout(@NotNull Doc doc) { return new Output(doc, Doc.empty()); }
     public static @NotNull Output stderr(@NotNull Doc doc) { return new Output(Doc.empty(), doc); }
     public static @NotNull Output stdout(@NotNull String doc) { return new Output(Doc.english(doc), Doc.empty()); }
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 33122c0998..36053870c7 100644
--- a/tools-repl/src/main/java/org/aya/repl/ReplUtil.java
+++ b/tools-repl/src/main/java/org/aya/repl/ReplUtil.java
@@ -1,25 +1,27 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.repl;
 
+import java.io.IOException;
+import java.nio.file.Path;
+import java.util.function.Consumer;
+
 import org.aya.pretty.doc.Doc;
+import org.aya.repl.Command.Output;
+import org.aya.repl.Command.Result;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 import org.jline.terminal.TerminalBuilder;
 import org.jline.utils.AttributedStringBuilder;
 import org.jline.utils.AttributedStyle;
 
-import java.io.IOException;
-import java.nio.file.Path;
-import java.util.function.Consumer;
-
 public interface ReplUtil {
-  static @NotNull Command.Result invokeHelp(CommandManager commandManager, @Nullable HelpItem argument) {
+  static @NotNull Result invokeHelp(CommandManager commandManager, @Nullable HelpItem argument) {
     if (argument != null && !argument.cmd.isEmpty()) {
       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));
+          it -> Result.ok(it.owner().help(), true),
+          () -> Result.err("No such command: " + argument.cmd, true));
     }
     var commands = Doc.vcat(commandManager.cmd.view()
       .map(command -> Doc.sep(
@@ -27,7 +29,7 @@ public interface ReplUtil {
         Doc.symbol("-"),
         Doc.english(command.owner().help())
       )));
-    return new Command.Result(new Command.Output(commands, Doc.empty()), true);
+    return new Result(Output.stdout(commands), true);
   }
 
   record HelpItem(@NotNull String cmd) {