diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java
index aa8a8bbab7..60ea166118 100644
--- a/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java
+++ b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java
@@ -108,7 +108,7 @@ public ImmutableSeq<ResolvingStmt> resolveStmt(@NotNull ImmutableSeq<Stmt> stmts
     return switch (predecl) {
       case DataDecl decl -> {
         var ctx = resolveTopLevelDecl(decl, context);
-        var innerCtx = resolveChildren(decl, ctx, d -> d.body.view(), (con, mCtx) -> {
+        var innerCtx = resolveChildren(decl, ctx, d -> d.body.clauses.view(), (con, mCtx) -> {
           setupModule(mCtx, con.ref);
           mCtx.defineSymbol(con.ref(), Stmt.Accessibility.Public, con.sourcePos());
         });
diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java
index 7ca1d76408..d9741b22ce 100644
--- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java
+++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java
@@ -57,23 +57,14 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
         // Generalized works for simple bodies and signatures
         var resolver = resolveDeclSignature(info, new ExprResolver(ctx, true), decl, where);
         switch (decl.body) {
-          case FnBody.BlockBody(var cls, var elims, var rawElims) -> {
-            assert elims == null;
+          case FnBody.BlockBody body -> {
+            assert body.elims() == null;
             // introducing generalized variable is not allowed in clauses, hence we insert them before body resolving
             insertGeneralizedVars(decl, resolver);
-            var finalElims = rawElims.map(elim -> {
-              var result = resolver.resolve(new QualifiedID(elim.sourcePos(), elim.data()));
-              if (!(result instanceof LocalVar localVar)) {
-                return resolver.ctx().reportAndThrow(new NameProblem.UnqualifiedNameNotFoundError(resolver.ctx(),
-                  elim.data(), elim.sourcePos()));
-              }
-              // result is LocalVar -> result in telescope
-              return localVar;
-            });
-
+            resolveElim(resolver, body.inner());
             var clausesResolver = resolver.deriveRestrictive();
             clausesResolver.reference().append(new TyckOrder.Head(decl));
-            decl.body = new FnBody.BlockBody(cls.map(clausesResolver::clause), finalElims, rawElims);
+            decl.body = body.map(clausesResolver::clause);
             addReferences(info, new TyckOrder.Body(decl), clausesResolver);
           }
           case FnBody.ExprBody(var expr) -> {
@@ -87,6 +78,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
       case ResolvingStmt.TopDecl(DataDecl data, var ctx) -> {
         var resolver = resolveDeclSignature(info, new ExprResolver(ctx, true), data, Where.Head);
         insertGeneralizedVars(data, resolver);
+        resolveElim(resolver, data.body);
         data.body.forEach(con -> {
           var bodyResolver = resolver.deriveRestrictive();
           var mCtx = MutableValue.create(resolver.ctx());
@@ -98,8 +90,9 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
           addReferences(info, new TyckOrder.Head(con), bodyResolver);
           // No body no body but you!
         });
+
         addReferences(info, new TyckOrder.Body(data), resolver.reference().view()
-          .concat(data.body.map(TyckOrder.Body::new)));
+          .concat(data.body.clauses.map(TyckOrder.Body::new)));
       }
       case ResolvingStmt.TopDecl(ClassDecl decl, var ctx) -> {
         var resolver = new ExprResolver(ctx, false);
@@ -172,4 +165,23 @@ private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, Exp
   private static void insertGeneralizedVars(@NotNull TeleDecl decl, @NotNull ExprResolver resolver) {
     decl.telescope = decl.telescope.prependedAll(resolver.allowedGeneralizes().valuesView());
   }
+
+  private static <Cls> void resolveElim(@NotNull ExprResolver resolver, @NotNull MatchBody<Cls> body) {
+    if (body.elims() != null) {
+      // TODO: panic or just return?
+      return;
+    }
+
+    var resolved = body.rawElims.map(elim -> {
+      var result = resolver.resolve(new QualifiedID(elim.sourcePos(), elim.data()));
+      if (!(result instanceof LocalVar localVar)) {
+        return resolver.ctx().reportAndThrow(new NameProblem.UnqualifiedNameNotFoundError(resolver.ctx(),
+          elim.data(), elim.sourcePos()));
+      }
+      // result is LocalVar -> result in telescope
+      return localVar;
+    });
+
+    body.resolve(resolved);
+  }
 }
diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index 6356e2eba6..19cd7e1146 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -98,8 +98,11 @@ yield switch (fnDecl.body) {
             fnRef.signature = fnRef.signature.descent(zonker::zonk);
             yield factory.apply(Either.left(resultTerm));
           }
-          case FnBody.BlockBody(var clauses, var elims, _) -> {
+          case FnBody.BlockBody body -> {
+            var clauses = body.clauses();
+            var elims = body.elims();
             assert elims != null;
+
             var signature = fnRef.signature;
             // we do not load signature here, so we need a fresh ExprTycker
             var clauseTycker = new ClauseTycker.Worker(new ClauseTycker(tycker = mkTycker()),
@@ -137,8 +140,8 @@ yield switch (fnDecl.body) {
       }
       case DataDecl data -> {
         assert data.ref.signature != null;
-        for (var kon : data.body) checkHeader(kon);
-        yield new DataDef(data.ref, data.body.map(kon -> kon.ref.core));
+        for (var kon : data.body.clauses) checkHeader(kon);
+        yield new DataDef(data.ref, data.body.clauses.map(kon -> kon.ref.core));
       }
     };
     reporter.clearSuppress();
@@ -174,11 +177,11 @@ else fail(BadTypeError.doNotLike(tycker.state, result, signature.result(),
         fnRef.signature = teleTycker.checkSignature(fn.telescope, result);
 
         // For ExprBody, they will be zonked later
-        if (fn.body instanceof FnBody.BlockBody(var cls, _, _)) {
+        if (fn.body instanceof FnBody.BlockBody body) {
           tycker.solveMetas();
           var zonker = new Finalizer.Zonk<>(tycker);
           fnRef.signature = fnRef.signature.pusheen(tycker::whnf).descent(zonker::zonk);
-          if (fnRef.signature.params().isEmpty() && cls.isEmpty())
+          if (fnRef.signature.params().isEmpty() && body.clauses().isEmpty())
             fail(new NobodyError(decl.sourcePos(), fn.ref));
         }
       }
@@ -239,8 +242,11 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
 
     var wellPats = ImmutableSeq.<Pat>empty();
     if (con.patterns.isNotEmpty()) {
+      var resolvedElim = dataRef.concrete.body.elims();
+      assert resolvedElim != null;
+      var indicies = ClauseTycker.Worker.computeIndices(ownerBinds, resolvedElim);
       // do not do coverage check
-      var lhsResult = new ClauseTycker(tycker = mkTycker()).checkLhs(dataSig, null,
+      var lhsResult = new ClauseTycker(tycker = mkTycker()).checkLhs(dataSig, indicies,
         new Pattern.Clause(con.entireSourcePos(), con.patterns, Option.none()), false);
       if (lhsResult.hasError()) {
         return;
diff --git a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
index 6bb19e69a3..7ac9c44dfd 100644
--- a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
+++ b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
@@ -101,15 +101,29 @@ public record Worker(
         cl.paramSubst, cl.asSubst, cl.clause, cl.hasError));
       return parent.checkAllRhs(teleVars, lhsResult);
     }
+
     private @Nullable ImmutableIntSeq computeIndices() {
-      return elims.isEmpty() ? null : elims.mapToInt(ImmutableIntSeq.factory(),
-        teleVars::indexOf);
+      return computeIndices(teleVars, elims);
     }
+
     public @NotNull TyckResult checkNoClassify() {
       return parent.checkAllRhs(teleVars, parent.checkAllLhs(computeIndices(), signature, clauses.view(), isFn));
     }
+
+    public static @Nullable ImmutableIntSeq computeIndices(
+      @NotNull ImmutableSeq<LocalVar> teleVars,
+      @NotNull ImmutableSeq<LocalVar> elims
+    ) {
+      return elims.isEmpty() ? null : elims.mapToInt(ImmutableIntSeq.factory(),
+        teleVars::indexOf);
+    }
   }
 
+  @Override public @NotNull Reporter reporter() { return exprTycker.reporter; }
+  @Override public @NotNull TyckState state() { return exprTycker.state; }
+
+  // region tycking
+
   public @NotNull ImmutableSeq<LhsResult> checkAllLhs(
     @Nullable ImmutableIntSeq indices, @NotNull Signature signature,
     @NotNull SeqView<Pattern.Clause> clauses, boolean isFn
@@ -134,20 +148,6 @@ public record Worker(
     return new TyckResult(rhsResult, lhsError);
   }
 
-  @Override public @NotNull Reporter reporter() { return exprTycker.reporter; }
-  @Override public @NotNull TyckState state() { return exprTycker.state; }
-  private @NotNull PatternTycker newPatternTycker(
-    @Nullable ImmutableIntSeq indices,
-    @NotNull SeqView<Param> telescope
-  ) {
-    telescope = indices != null
-      ? telescope.mapIndexed((idx, p) -> indices.contains(idx) ? p.explicitize() : p.implicitize())
-      : telescope;
-
-    return new PatternTycker(exprTycker, telescope, new LocalLet(), indices == null,
-      new Renamer());
-  }
-
   public @NotNull LhsResult checkLhs(
     @NotNull Signature signature,
     @Nullable ImmutableIntSeq indices,
@@ -226,6 +226,36 @@ else if (result.hasError) {
     }
   }
 
+  // endregion tycking
+
+  // region util
+
+  private @NotNull PatternTycker newPatternTycker(
+    @Nullable ImmutableIntSeq indices,
+    @NotNull SeqView<Param> telescope
+  ) {
+    telescope = indices != null
+      ? telescope.mapIndexed((idx, p) -> indices.contains(idx) ? p.explicitize() : p.implicitize())
+      : telescope;
+
+    return new PatternTycker(exprTycker, telescope, new LocalLet(), indices == null,
+      new Renamer());
+  }
+
+  private static boolean hasAbsurdity(@NotNull Pattern term) {
+    return hasAbsurdity(term, MutableBooleanValue.create());
+  }
+
+  private static boolean hasAbsurdity(@NotNull Pattern term, @NotNull MutableBooleanValue b) {
+    if (term == Pattern.Absurd.INSTANCE) b.set(true);
+    else term.forEach((_, p) -> b.set(b.get() || hasAbsurdity(p, b)));
+    return b.get();
+  }
+
+  // endregion util
+
+  // region post tycking
+
   private static final class TermInline implements UnaryOperator<Term> {
     @Override public @NotNull Term apply(@NotNull Term term) {
       if (term instanceof MetaPatTerm metaPat) {
@@ -239,14 +269,6 @@ private static final class TermInline implements UnaryOperator<Term> {
     }
   }
 
-  private static boolean hasAbsurdity(@NotNull Pattern term) {
-    return hasAbsurdity(term, MutableBooleanValue.create());
-  }
-  private static boolean hasAbsurdity(@NotNull Pattern term, @NotNull MutableBooleanValue b) {
-    if (term == Pattern.Absurd.INSTANCE) b.set(true);
-    else term.forEach((_, p) -> b.set(b.get() || hasAbsurdity(p, b)));
-    return b.get();
-  }
 
   /**
    * Inline terms which in pattern
@@ -285,4 +307,6 @@ public static void apply(@NotNull Pattern pat) {
 
     return new PatternTycker.TyckResult(wellTyped, paramSubst, result.asSubst(), result.newBody(), result.hasError());
   }
+
+  // endregion post tycking
 }
diff --git a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java
index 99807275bd..33bd9a8064 100644
--- a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java
+++ b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java
@@ -487,7 +487,7 @@ private record Selection(
       case DataDef.Delegate delegate -> {
         // the core may be unchecked!
         var concrete = (DataDecl) delegate.ref.concrete;
-        yield concrete.body.view()
+        yield concrete.body.clauses.view()
           .filter(it -> it.telescope.isEmpty())
           .map(it -> it.ref.name());
       }
diff --git a/base/src/test/java/org/aya/syntax/concrete/SyntaxTest.java b/base/src/test/java/org/aya/syntax/concrete/SyntaxTest.java
index 8d04df5dc2..2a53e3768b 100644
--- a/base/src/test/java/org/aya/syntax/concrete/SyntaxTest.java
+++ b/base/src/test/java/org/aya/syntax/concrete/SyntaxTest.java
@@ -25,6 +25,9 @@ def bar (A : Type 0) : A -> A => fn x => {? x ?}
       open inductive Fin Nat
       | S n => FZ
       | S n => FS (Fin n)
+      open inductive Vec (A : Type) (n : Nat) elim n
+      | O => vnil
+      | S m => vcons A (Vec A m)
       def infixl + Nat Nat : Nat
       | 0, a => a
       | S a, b as b' => S (a + b')
diff --git a/cli-impl/src/test/resources/shared/src/data/vec/base.aya b/cli-impl/src/test/resources/shared/src/data/vec/base.aya
index 140730357a..74d37c30b2 100644
--- a/cli-impl/src/test/resources/shared/src/data/vec/base.aya
+++ b/cli-impl/src/test/resources/shared/src/data/vec/base.aya
@@ -1,8 +1,9 @@
 open import prelude hiding (++)
 
-open inductive Vec Nat Type
-| 0, A => []
-| suc n, A => infixr :> A (Vec n A)
+@suppress(Shadowing)
+open inductive Vec (n : Nat) (A : Type) elim n
+| 0 => []
+| suc n => infixr :> A (Vec n A)
 
 variable A B : Type
 variable n m o : Nat
diff --git a/ide/src/main/java/org/aya/ide/Resolver.java b/ide/src/main/java/org/aya/ide/Resolver.java
index 1c070af01b..eae86e7949 100644
--- a/ide/src/main/java/org/aya/ide/Resolver.java
+++ b/ide/src/main/java/org/aya/ide/Resolver.java
@@ -73,7 +73,7 @@ public interface Resolver {
 
   static @NotNull SeqView<DefVar<?, ?>> withChildren(@NotNull Decl def) {
     return switch (def) {
-      case DataDecl data -> SeqView.<DefVar<?, ?>>of(data.ref).appendedAll(data.body.map(DataCon::ref));
+      case DataDecl data -> SeqView.<DefVar<?, ?>>of(data.ref).appendedAll(data.body.clauses.map(DataCon::ref));
       // case ClassDecl struct ->
       //   SeqView.<DefVar<?, ?>>of(struct.ref).appendedAll(struct.members.map(TeleDecl.ClassMember::ref));
       default -> SeqView.of(def.ref());
diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java
index 7562ba4902..25c730970b 100644
--- a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java
+++ b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java
@@ -41,6 +41,7 @@ public interface AyaPsiElementTypes {
   IElementType DO_BINDING = new AyaPsiElementType("DO_BINDING");
   IElementType DO_BLOCK_CONTENT = new AyaPsiElementType("DO_BLOCK_CONTENT");
   IElementType DO_EXPR = new AyaPsiElementType("DO_EXPR");
+  IElementType ELIM_DATA_BODY = new AyaPsiElementType("ELIM_DATA_BODY");
   IElementType EXPR = new AyaPsiElementType("EXPR");
   IElementType FN_BODY = new AyaPsiElementType("FN_BODY");
   IElementType FN_DECL = new AyaPsiElementType("FN_DECL");
diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
index 29fab8c069..b28c1d23d2 100644
--- a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
+++ b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
@@ -693,7 +693,7 @@ public static boolean dataConClause(PsiBuilder b, int l) {
   /* ********************************************************** */
   // pragma* declModifier*
   //  KW_DATA declNameOrInfix?
-  //  tele* type? bindBlock? dataBody*
+  //  tele* type? bindBlock? elimDataBody
   public static boolean dataDecl(PsiBuilder b, int l) {
     if (!recursion_guard_(b, l, "dataDecl")) return false;
     boolean r, p;
@@ -706,7 +706,7 @@ public static boolean dataDecl(PsiBuilder b, int l) {
     r = p && report_error_(b, dataDecl_4(b, l + 1)) && r;
     r = p && report_error_(b, dataDecl_5(b, l + 1)) && r;
     r = p && report_error_(b, dataDecl_6(b, l + 1)) && r;
-    r = p && dataDecl_7(b, l + 1) && r;
+    r = p && elimDataBody(b, l + 1) && r;
     exit_section_(b, l, m, r, p, null);
     return r || p;
   }
@@ -765,17 +765,6 @@ private static boolean dataDecl_6(PsiBuilder b, int l) {
     return true;
   }
 
-  // dataBody*
-  private static boolean dataDecl_7(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "dataDecl_7")) return false;
-    while (true) {
-      int c = current_position_(b);
-      if (!dataBody(b, l + 1)) break;
-      if (!empty_element_parsed_guard_(b, "dataDecl_7", c)) break;
-    }
-    return true;
-  }
-
   /* ********************************************************** */
   // fnDecl | primDecl | classDecl | dataDecl
   public static boolean decl(PsiBuilder b, int l) {
@@ -862,6 +851,36 @@ public static boolean doBlockContent(PsiBuilder b, int l) {
     return r;
   }
 
+  /* ********************************************************** */
+  // elims? dataBody*
+  public static boolean elimDataBody(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "elimDataBody")) return false;
+    boolean r;
+    Marker m = enter_section_(b, l, _NONE_, ELIM_DATA_BODY, "<elim data body>");
+    r = elimDataBody_0(b, l + 1);
+    r = r && elimDataBody_1(b, l + 1);
+    exit_section_(b, l, m, r, false, null);
+    return r;
+  }
+
+  // elims?
+  private static boolean elimDataBody_0(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "elimDataBody_0")) return false;
+    elims(b, l + 1);
+    return true;
+  }
+
+  // dataBody*
+  private static boolean elimDataBody_1(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "elimDataBody_1")) return false;
+    while (true) {
+      int c = current_position_(b);
+      if (!dataBody(b, l + 1)) break;
+      if (!empty_element_parsed_guard_(b, "elimDataBody_1", c)) break;
+    }
+    return true;
+  }
+
   /* ********************************************************** */
   // KW_ELIM weakId+
   static boolean elims(PsiBuilder b, int l) {
diff --git a/parser/src/main/grammar/AyaPsiParser.bnf b/parser/src/main/grammar/AyaPsiParser.bnf
index 7ebd42c282..b40be7b3e5 100644
--- a/parser/src/main/grammar/AyaPsiParser.bnf
+++ b/parser/src/main/grammar/AyaPsiParser.bnf
@@ -239,7 +239,9 @@ classMember
 
 dataDecl ::= pragma* declModifier*
  KW_DATA declNameOrInfix?
- tele* type? bindBlock? dataBody* { pin=3 }
+ tele* type? bindBlock? elimDataBody { pin=3 }
+
+elimDataBody ::= elims? dataBody*
 
 dataBody ::= BAR (dataConClause | dataCon) {
   mixin="org.aya.intellij.psi.impl.AyaPsiGenericDeclImpl"
diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java
index 1ca70a538d..f4663a6f78 100644
--- a/producer/src/main/java/org/aya/producer/AyaProducer.java
+++ b/producer/src/main/java/org/aya/producer/AyaProducer.java
@@ -335,7 +335,7 @@ private void pragma(GenericNode<?> node, Decl decl) {
     var elims = node.childrenOfType(WEAK_ID)
       .map(this::weakId)
       .toImmutableSeq();
-    return new FnBody.BlockBody(body, null, elims);
+    return new FnBody.BlockBody(body, elims);
   }
 
   private void giveMeOpen(@NotNull ModifierParser.Modifiers modiSet, @NotNull Decl decl, @NotNull MutableList<Stmt> additional) {
@@ -353,19 +353,28 @@ private void giveMeOpen(@NotNull ModifierParser.Modifiers modiSet, @NotNull Decl
   }
 
   public @Nullable DataDecl dataDecl(GenericNode<?> node, @NotNull MutableList<Stmt> additional) {
-    var body = node.childrenOfType(DATA_BODY).mapNotNull(this::dataBody).toImmutableSeq();
+    var body = node.peekChild(ELIM_DATA_BODY);
+    if (body == null) return error(body, "Expect data body");
     var tele = telescope(node.childrenOfType(TELE));
     var info = declInfo(node, ModifierParser.DECL_FILTER);
     var name = info.checkName(this);
     if (name == null) return null;
     var ty = typeOrNull(node.peekChild(TYPE));
-    var decl = new DataDecl(info.info, name, tele, ty, body);
+    var decl = new DataDecl(info.info, name, tele, ty, elimDataBody(body));
     if (info.modifier.isExample()) decl.isExample = true;
     giveMeOpen(info.modifier, decl, additional);
     pragma(node, decl);
     return decl;
   }
 
+  public @NotNull MatchBody<DataCon> elimDataBody(@NotNull GenericNode<?> node) {
+    var elims = node.childrenOfType(WEAK_ID)
+      .map(this::weakId)
+      .toImmutableSeq();
+    var bodies = node.childrenOfType(DATA_BODY).mapNotNull(this::dataBody).toImmutableSeq();
+    return new MatchBody<>(bodies, elims);
+  }
+
   public @Nullable DataCon dataBody(@NotNull GenericNode<?> node) {
     var dataConClause = node.peekChild(DATA_CON_CLAUSE);
     if (dataConClause != null) return dataCon(
diff --git a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
index 071327747c..ad0158652a 100644
--- a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
@@ -32,6 +32,7 @@
 
 import java.util.Locale;
 import java.util.Objects;
+import java.util.function.Function;
 
 import static org.aya.prettier.Tokens.*;
 
@@ -340,10 +341,7 @@ private Doc visitAccess(@NotNull Accessibility acc, @Nullable Accessibility theD
         yield Doc.cat(Doc.sepNonEmpty(prelude),
           switch (decl.body) {
             case FnBody.ExprBody(var expr) -> Doc.cat(Doc.spaced(FN_DEFINED_AS), term(Outer.Free, expr));
-            case FnBody.BlockBody(var clauses, var elims, var raw) -> Doc.vcat(
-              Doc.cat(Doc.spaced(KW_ELIM),
-                Doc.commaList(elims == null ? raw.map(name -> Doc.plain(name.data())) : elims.map(BasePrettier::varDoc))),
-              Doc.nest(2, visitClauses(clauses)));
+            case FnBody.BlockBody(var inner) -> visitMatchBody(inner, cls -> Doc.nest(2, visitClauses(cls)));
           },
           visitBindBlock(decl.bindBlock())
         );
@@ -355,8 +353,8 @@ private Doc visitAccess(@NotNull Accessibility acc, @Nullable Accessibility theD
         prelude.append(visitTele(decl.telescope));
         appendResult(prelude, decl.result);
         yield Doc.cat(Doc.sepNonEmpty(prelude),
-          Doc.emptyIf(decl.body.isEmpty(), () -> Doc.cat(Doc.line(), Doc.nest(2, Doc.vcat(
-            decl.body.view().map(this::decl))))),
+          visitMatchBody(decl.body, cons ->
+            Doc.nest(2, Doc.vcat(cons.map(this::decl)))),
           visitBindBlock(decl.bindBlock())
         );
       }
@@ -427,6 +425,22 @@ else if (tighters.isEmpty()) return Doc.cat(Doc.line(), Doc.hang(2, Doc.sep(
     )))));
   }
 
+  /// @param prettier invoked when the clauses is not empty
+  private <Cls> @NotNull Doc visitMatchBody(@NotNull MatchBody<Cls> body, @NotNull Function<ImmutableSeq<Cls>, Doc> prettier) {
+    Doc elimLine = Doc.empty();
+
+    if (body.rawElims.isNotEmpty()) {
+      var elim = body.elims();
+      var elimList = elim == null
+        ? body.rawElims.map(x -> Doc.plain(x.data()))
+        : elim.map(BasePrettier::varDoc);
+      elimLine = Doc.cat(Doc.spaced(KW_ELIM), Doc.sep(elimList));
+    }
+
+    var clauses = Doc.emptyIf(body.clauses.isEmpty(), () -> prettier.apply(body.clauses));
+    return Doc.vcat(elimLine, clauses);
+  }
+
   private @NotNull Doc visitLetBind(@NotNull Expr.LetBind letBind) {
     // f : G := g
     var prelude = MutableList.of(varDoc(letBind.bindName()));
diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/StmtVisitor.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/StmtVisitor.java
index df87ce730b..97326c5c39 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/stmt/StmtVisitor.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/stmt/StmtVisitor.java
@@ -106,7 +106,7 @@ default void accept(@NotNull Stmt stmt) {
       case Decl decl -> {
         if (decl instanceof TeleDecl tele) visitTelescopic(tele);
         switch (decl) {
-          case DataDecl data -> data.body.forEach(this);
+          case DataDecl data -> data.body.forEach(this::accept);
           case ClassDecl clazz -> clazz.members.forEach(this);
           case FnDecl fn -> {
             fn.body.forEach(this::visitExpr, cl -> cl.forEach(this::visitExpr,
diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/DataDecl.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/DataDecl.java
index 460552b393..770c84e169 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/DataDecl.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/DataDecl.java
@@ -20,14 +20,14 @@
  */
 public final class DataDecl extends TeleDecl {
   public final @NotNull DefVar<DataDef, DataDecl> ref;
-  public final @NotNull ImmutableSeq<DataCon> body;
+  public final @NotNull MatchBody<DataCon> body;
 
   public DataDecl(
     @NotNull DeclInfo info,
     @NotNull String name,
     @NotNull ImmutableSeq<Expr.Param> telescope,
     @Nullable WithPos<Expr> result,
-    @NotNull ImmutableSeq<DataCon> body
+    @NotNull MatchBody<DataCon> body
   ) {
     super(info, telescope, result);
     this.body = body;
diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/FnBody.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/FnBody.java
index ffa1392ffb..09f84d56b1 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/FnBody.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/FnBody.java
@@ -27,19 +27,36 @@ record ExprBody(@NotNull WithPos<Expr> expr) implements FnBody {
     }
   }
 
-  /**
-   * @param elims NotNull after resolving
-   */
-  record BlockBody(
-    @NotNull ImmutableSeq<Pattern.Clause> clauses,
-    @Nullable ImmutableSeq<LocalVar> elims,
-    @NotNull ImmutableSeq<WithPos<String>> rawElims
-  ) implements FnBody {
+  record BlockBody(@NotNull MatchBody<Pattern.Clause> inner) implements FnBody {
+    public BlockBody(
+      @NotNull ImmutableSeq<Pattern.Clause> clauses,
+      @NotNull ImmutableSeq<WithPos<String>> rawElims
+    ) {
+      this(new MatchBody<>(clauses, rawElims));
+    }
+
+    public @NotNull ImmutableSeq<Pattern.Clause> clauses() {
+      return inner.clauses;
+    }
+
+    public @Nullable ImmutableSeq<LocalVar> elims() {
+      return inner.elims();
+    }
+
+    public @NotNull ImmutableSeq<WithPos<String>> rawElims() {
+      return inner.rawElims;
+    }
+
+    public @NotNull BlockBody map(@NotNull UnaryOperator<Pattern.Clause> f) {
+      return new BlockBody(inner.descent(f));
+    }
+
     @Override public BlockBody map(@NotNull PosedUnaryOperator<Expr> f, @NotNull UnaryOperator<Pattern.Clause> g) {
-      return new BlockBody(clauses.map(g), elims, rawElims);
+      return new BlockBody(inner.descent(g));
     }
+
     @Override public void forEach(@NotNull PosedConsumer<Expr> f, @NotNull Consumer<Pattern.Clause> g) {
-      clauses.forEach(g);
+      clauses().forEach(g);
     }
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/MatchBody.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/MatchBody.java
new file mode 100644
index 0000000000..7c42da4266
--- /dev/null
+++ b/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/MatchBody.java
@@ -0,0 +1,55 @@
+// Copyright (c) 2020-2024 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.concrete.stmt.decl;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.syntax.ref.LocalVar;
+import org.aya.util.error.WithPos;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+import java.util.function.Consumer;
+import java.util.function.UnaryOperator;
+
+public class MatchBody<Clause> {
+  public final @NotNull ImmutableSeq<Clause> clauses;
+  public final @NotNull ImmutableSeq<WithPos<String>> rawElims;
+  private @Nullable ImmutableSeq<LocalVar> elims;
+
+  private MatchBody(
+    @NotNull ImmutableSeq<Clause> clauses,
+    @NotNull ImmutableSeq<WithPos<String>> rawElims,
+    @Nullable ImmutableSeq<LocalVar> elims
+  ) {
+    this.clauses = clauses;
+    this.rawElims = rawElims;
+    this.elims = elims;
+  }
+
+  public MatchBody(@NotNull ImmutableSeq<Clause> clauses, @NotNull ImmutableSeq<WithPos<String>> rawElims) {
+    this(clauses, rawElims, null);
+  }
+
+  public @Nullable ImmutableSeq<LocalVar> elims() {
+    return elims;
+  }
+
+  public @NotNull MatchBody<Clause> update(@NotNull ImmutableSeq<Clause> clauses) {
+    return this.clauses.sameElements(clauses, true)
+      ? this
+      : new MatchBody<>(clauses, rawElims, elims);
+  }
+
+  public void resolve(@NotNull ImmutableSeq<LocalVar> elims) {
+    assert this.elims == null;
+    this.elims = elims;
+  }
+
+  public @NotNull MatchBody<Clause> descent(@NotNull UnaryOperator<Clause> f) {
+    return update(clauses.map(f));
+  }
+
+  public void forEach(@NotNull Consumer<Clause> f) {
+    clauses.forEach(f);
+  }
+}