diff --git a/base/src/main/java/org/aya/resolve/ResolvingStmt.java b/base/src/main/java/org/aya/resolve/ResolvingStmt.java
index 96c295fac..ee273a1d8 100644
--- a/base/src/main/java/org/aya/resolve/ResolvingStmt.java
+++ b/base/src/main/java/org/aya/resolve/ResolvingStmt.java
@@ -17,12 +17,12 @@
  *   postulate
  *     Context : Set
  *
- *   data Stmt : Set where
+ *   inductive Stmt : Set where
  *     FnDecl : Stmt
  *     DataDecl : Stmt
  *     DataCon : Stmt
  *
- *   data ExtInfo : Stmt -> Set where
+ *   inductive ExtInfo : Stmt -> Set where
  *     ExtData : Context -> ExtInfo DataDecl
  *     ExtFn : Context -> ExtInfo FnDecl
  *     -- trivial extra info
diff --git a/base/src/test/java/org/aya/tyck/PatternTyckTest.java b/base/src/test/java/org/aya/tyck/PatternTyckTest.java
index b6ea1d875..19d7e3102 100644
--- a/base/src/test/java/org/aya/tyck/PatternTyckTest.java
+++ b/base/src/test/java/org/aya/tyck/PatternTyckTest.java
@@ -18,7 +18,7 @@
 public class PatternTyckTest {
   @Test public void elim0() {
     var result = tyck("""
-      open data Nat | O | S Nat
+      open inductive Nat | O | S Nat
       def lind (a b : Nat) : Nat elim a
       | 0 => b
       | S a' => S (lind a' b)
@@ -28,8 +28,8 @@ def lind (a b : Nat) : Nat elim a
 
   @Test public void test1() {
     var result = tyck("""
-      open data Nat | O | S Nat
-      open data Vec Nat Type
+      open inductive Nat | O | S Nat
+      open inductive Vec Nat Type
       | 0, A => vnil
       | S n, A => infixr vcons A (Vec n A)
       
@@ -52,7 +52,7 @@ def unwrap (A : Type) (v : Vec 1 A) : A elim v
 
   @Test public void test2() {
     var result = tyck("""
-      open data Nat | O | S Nat
+      open inductive Nat | O | S Nat
       
       prim I : ISet
       prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
@@ -79,7 +79,7 @@ def pmap (f : A -> B) {a b : A} (p : a = b) : f a = f b => \\i => f (p i)
 
   @Test public void test3() {
     var result = tyck("""
-      open data Nat | O | S Nat
+      open inductive Nat | O | S Nat
       
       prim I : ISet
       prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
@@ -94,7 +94,7 @@ prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
       | a, S b => S (a +' b)
       tighter =
       
-      open data Int
+      open inductive Int
       | pos Nat | neg Nat
       | zro : pos 0 = neg 0
       
@@ -114,8 +114,8 @@ prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
 
   @Test public void test4() {
     assertTrue(tyck("""
-      open data Nat | O | S Nat
-      open data Fin Nat
+      open inductive Nat | O | S Nat
+      open inductive Fin Nat
       | 1 => fzero
       | S n => fsucc (Fin n)
       
@@ -125,8 +125,8 @@ def exfalso (A : Type) (x : Fin 0) : A elim x | ()
 
   @Test public void issue630() {
     assertTrue(tyck("""
-      open data Nat | O | S Nat
-      open data INat (n : Nat)
+      open inductive Nat | O | S Nat
+      open inductive INat (n : Nat)
       | O => zero
       | S n' => +-one
       | S (S n') => +-two
@@ -140,12 +140,12 @@ open data INat (n : Nat)
   @Test
   public void test5() {
     @Language("Aya") var code = """
-      open data Nat | O | S Nat
-      open data Vec Type Nat
+      open inductive Nat | O | S Nat
+      open inductive Vec Type Nat
       | A, O => vnil
       | A, S n => vcons A (Vec A n)
-            
-      open data MatchMe (n : Nat) (Vec Nat n)
+      
+      open inductive MatchMe (n : Nat) (Vec Nat n)
       | S n', vcons v xs => matched
 
       def checkMe {n : Nat} (m : Nat) {v : Vec Nat n} (MatchMe n v) : Nat
diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java
index 71340ebd7..df10ba312 100644
--- a/base/src/test/java/org/aya/tyck/TyckTest.java
+++ b/base/src/test/java/org/aya/tyck/TyckTest.java
@@ -3,37 +3,21 @@
 package org.aya.tyck;
 
 import kala.collection.immutable.ImmutableSeq;
-import kala.collection.immutable.primitive.ImmutableIntSeq;
-import org.aya.normalize.Normalizer;
-import org.aya.primitive.PrimFactory;
 import org.aya.resolve.ResolveInfo;
 import org.aya.resolve.module.ModuleCallback;
 import org.aya.syntax.SyntaxTestUtil;
-import org.aya.syntax.core.Closure;
-import org.aya.syntax.core.def.*;
-import org.aya.syntax.core.term.LamTerm;
-import org.aya.syntax.core.term.Term;
-import org.aya.syntax.core.term.call.DataCall;
-import org.aya.syntax.core.term.call.FnCall;
-import org.aya.syntax.core.term.repr.IntegerTerm;
-import org.aya.syntax.core.term.repr.ListTerm;
-import org.aya.syntax.literate.CodeOptions;
+import org.aya.syntax.core.def.TyckDef;
 import org.intellij.lang.annotations.Language;
 import org.jetbrains.annotations.NotNull;
 import org.junit.jupiter.api.Test;
 
-import java.util.Random;
-import java.util.function.Function;
-import java.util.function.IntFunction;
-
-import static org.junit.jupiter.api.Assertions.assertNotNull;
 import static org.junit.jupiter.api.Assertions.assertTrue;
 
 public class TyckTest {
   @Test public void test0() {
     var result = tyck("""
-      data Nat | O | S Nat
-      data FreeMonoid (A : Type) | e | cons A (FreeMonoid A)
+      inductive Nat | O | S Nat
+      inductive FreeMonoid (A : Type) | e | cons A (FreeMonoid A)
       
       def id {A : Type} (a : A) => a
       def lam (A : Type) : Fn (a : A) -> Type => fn a => A
@@ -47,7 +31,7 @@ def letExample (A : Type) (B : A -> Type) (f : Fn (a : A) -> B a) (a : A) : B a
 
   @Test public void test1() {
     var result = tyck("""
-      open data Unit | unit
+      open inductive Unit | unit
       variable A : Type
       def foo {value : A} : A => value
       def what : Unit => foo {value := unit}
@@ -57,7 +41,7 @@ def letExample (A : Type) (B : A -> Type) (f : Fn (a : A) -> B a) (a : A) : B a
 
   @Test public void path0() {
     var result = tyck("""
-      data Nat
+      inductive Nat
       | O : Nat
       | S (x : Nat) : Nat
       prim I : ISet
@@ -73,14 +57,14 @@ def coeFill0 (A : I -> Type) (u : A 0) : Path A u (transp A u) => \\i => coe 0 i
 
   @Test public void path1() {
     var result = tyck("""
-      data Nat | O | S Nat
+      inductive Nat | O | S Nat
       prim I : ISet
       prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
       prim coe
       variable A : Type
       def infix = (a b : A) => Path (\\i => A) a b
       def refl {a : A} : a = a => \\i => a
-      open data Int
+      open inductive Int
       | pos Nat | neg Nat
       | zro : pos 0 = neg 0
       example def testZro0 : zro 0 = pos 0 => refl
@@ -96,9 +80,9 @@ def funExt (A B : Type) (f g : A -> B) (p : Fn (a : A) -> f a = g a) : f = g =>
   /*@Test*/
   public void issue768() {
     var result = tyck("""
-      open data Unit | unit
-      data Nat | O | S Nat
-      open data SomeDT Nat
+      open inductive Unit | unit
+      inductive Nat | O | S Nat
+      open inductive SomeDT Nat
       | m => someDT
       def how' {m : Nat} (a : Nat) (b : SomeDT m) : Nat => 0
       def what {A : Nat -> Type} (B : Fn (n : Nat) -> A n -> Nat) : Unit => unit
@@ -109,8 +93,8 @@ public void issue768() {
 
   @Test public void test2() {
     var result = tyck("""
-      open data Nat | O | S Nat
-      open data Bool | true | false
+      open inductive Nat | O | S Nat
+      open inductive Bool | true | false
       def not Bool : Bool | true => false | false => true
       def even Nat : Bool
       | 0 => true
@@ -124,113 +108,15 @@ public void issue768() {
 
   @Test public void test3() {
     assertTrue(tyck("""
-      open data Nat | O | S Nat
-      open data Natt | OO | SS Nat
+      open inductive Nat | O | S Nat
+      open inductive Natt | OO | SS Nat
       def infix = {A : Type} (a b : A) => Type
       // Disambiguate by type checking
       def test (a : Nat) => a = 114514
       """).defs.isNotEmpty());
   }
 
-  @Test
-  public void sort() {
-    var result = tyck("""
-      open data Nat | O | S Nat
-      open data Bool | True | False
-      open data List Type
-      | nil
-      | A => infixr cons A (List A)
-            
-      open data Color | red | black
-      def Decider (A : Type) => Fn (x y : A) -> Bool
-            
-      variable A : Type
-            
-      open data RBTree (A : Type) : Type
-      | rbLeaf
-      | rbNode Color (RBTree A) A (RBTree A)
-            
-      def rbTreeToList (rb : RBTree A) (r : List A) : List A elim rb
-      | rbLeaf => r
-      | rbNode x t1 a t2 => rbTreeToList t1 (a cons rbTreeToList t2 r)
-            
-      def repaint (RBTree A) : RBTree A
-      | rbNode c l a r => rbNode black l a r
-      | rbLeaf => rbLeaf
-
-      def le (x y : Nat) : Bool
-      | O, _ => True
-      | S _, O => False
-      | S a, S b => le a b
-            
-      def balanceLeft Color (RBTree A) A (RBTree A) : RBTree A
-      | black, rbNode red (rbNode red a x b) y c, v, r =>
-          rbNode red (rbNode black a x b) y (rbNode black c v r)
-      | black, rbNode red a x (rbNode red b y c), v, r =>
-          rbNode red (rbNode black a x b) y (rbNode black c v r)
-      | c, a, v, r => rbNode c a v r
-            
-      def balanceRight Color (RBTree A) A (RBTree A) : RBTree A
-      | black, l, v, rbNode red (rbNode red b y c) z d =>
-          rbNode red (rbNode black l v b) y (rbNode black c z d)
-      | black, l, v, rbNode red b y (rbNode red c z d) =>
-          rbNode red (rbNode black l v b) y (rbNode black c z d)
-      | c, l, v, b => rbNode c l v b
-
-      def insert_lemma (dec_le : Decider A) (a a1 : A) (c : Color) (l1 l2 : RBTree A) (b : Bool) : RBTree A elim b
-      | True => balanceRight c l1 a1 (insert a l2 dec_le)
-      | False => balanceLeft c (insert a l1 dec_le) a1 l2
-
-      def insert (a : A) (node : RBTree A) (dec_le : Decider A) : RBTree A elim node
-      | rbLeaf => rbNode red rbLeaf a rbLeaf
-      | rbNode c l1 a1 l2 => insert_lemma dec_le a a1 c l1 l2 (dec_le a1 a)
-
-      private def aux (l : List A) (r : RBTree A) (dec_le : Decider A) : RBTree A elim l
-      | nil => r
-      | a cons l => aux l (repaint (insert a r dec_le)) dec_le
-      def tree_sort (dec_le : Decider A) (l : List A) => rbTreeToList (aux l rbLeaf dec_le) nil
-      """);
-
-    var defs = result.defs;
-
-    var Nat = (DataDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("Nat")).get());
-    var O = (ConDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("O")).get());
-    var S = (ConDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("S")).get());
-    var List = (DataDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("List")).get());
-    var nil = (ConDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("nil")).get());
-    var cons = (ConDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("cons")).get());
-    var le = (FnDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("le")).get());
-    var tree_sort = (FnDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("tree_sort")).get());
-
-    var NatCall = new DataCall(Nat, 0, ImmutableSeq.empty());
-    var ListNatCall = new DataCall(List, 0, ImmutableSeq.of(NatCall));
-
-    IntFunction<Term> mkInt = i -> new IntegerTerm(i, O, S, NatCall);
-
-    Function<ImmutableIntSeq, Term> mkList = xs -> new ListTerm(xs.mapToObj(mkInt::apply), nil, cons, ListNatCall);
-
-    var leCall = new LamTerm(new Closure.Jit(x ->
-      new LamTerm(new Closure.Jit(y ->
-        new FnCall(le, 0, ImmutableSeq.of(x, y))))));
-
-    var seed = 114514L;
-    var random = new Random(seed);
-    var largeList = mkList.apply(ImmutableIntSeq.fill(50, () -> Math.abs(random.nextInt()) % 100));
-    var args = ImmutableSeq.of(NatCall, leCall, largeList);
-
-    var beginTime = System.currentTimeMillis();
-    var sortResult = new Normalizer(new TyckState(result.info().shapeFactory(), new PrimFactory()))
-      .normalize(new FnCall(tree_sort, 0, args), CodeOptions.NormalizeMode.FULL);
-    var endTime = System.currentTimeMillis();
-    assertNotNull(sortResult);
-
-    System.out.println(STR."Done in \{(endTime - beginTime)}");
-    System.out.println(sortResult.debuggerOnlyToString());
-  }
-
-  public record TyckResult(@NotNull ImmutableSeq<TyckDef> defs, @NotNull ResolveInfo info) {
-
-  }
+  public record TyckResult(@NotNull ImmutableSeq<TyckDef> defs, @NotNull ResolveInfo info) { }
 
   public static TyckResult tyck(@Language("Aya") @NotNull String code) {
     var moduleLoader = SyntaxTestUtil.moduleLoader();
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 5d56f2901..9e7145b97 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
@@ -38,12 +38,12 @@ public class ReplCompilerTest {
 
   @Test public void issue382() {
     // success cases, we can find the definition in the context
-    compile("data Nat | zero | suc Nat");
+    compile("inductive Nat | zero | suc Nat");
     var nat = findContext("Nat");
     assertNotNull(nat);
 
     // failure cases, the context is unchanged
-    assertThrows(Throwable.class, () -> compile("data Nat ="));
+    assertThrows(Throwable.class, () -> compile("inductive Nat ="));
     var newNat = findContext("Nat");
     assertEquals(nat, newNat);
 
@@ -54,9 +54,9 @@ public class ReplCompilerTest {
   /** <a href="https://ice1000.jetbrains.space/im/group/4DLh053zIix6?message=2db0002db&channel=4DLh053zIix6">Bug report</a> */
   @Test public void reportedInSpace() {
     // success cases, we can find the definition in the context
-    compile("data Unit | unit");
+    compile("inductive Unit | unit");
     assertNotNull(findContext("Unit"));
-    compile("data What | what");
+    compile("inductive What | what");
     assertNotNull(findContext("What"));
     assertNotNull(findContext("Unit"));
   }
diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/ExprTyckError.java b/cli-impl/src/test/java/org/aya/test/fixtures/ExprTyckError.java
index be33fbea6..edef3de45 100644
--- a/cli-impl/src/test/java/org/aya/test/fixtures/ExprTyckError.java
+++ b/cli-impl/src/test/java/org/aya/test/fixtures/ExprTyckError.java
@@ -34,14 +34,14 @@ prim Path (A : I -> Type) (a b : A)
     """;
 
   @Language("Aya") String testPiDom = """
-    data X : Set
-    data Test : Type | con X
+    inductive X : Set
+    inductive Test : Type | con X
     """;
 
   @Language("Aya") String testPiDomMeta = """
-    data X : Set
-    data infix = (a b : X) : Type
-    data Test : Type
+    inductive X : Set
+    inductive infix = (a b : X) : Type
+    inductive Test : Type
     | con (x : _) (y : X) (x = y)
     """;
 }
diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/GoalAndMeta.java b/cli-impl/src/test/java/org/aya/test/fixtures/GoalAndMeta.java
index d980467dd..060685225 100644
--- a/cli-impl/src/test/java/org/aya/test/fixtures/GoalAndMeta.java
+++ b/cli-impl/src/test/java/org/aya/test/fixtures/GoalAndMeta.java
@@ -18,16 +18,16 @@ def test (a : Nat) : Nat => {? a ?}
 
   @Language("Aya") String testUnsolvedMetaLit = """
     open import arith::Nat
-    open data Nat2 | OO | SS Nat2
-    open data Option (A : Type)
+    open inductive Nat2 | OO | SS Nat2
+    open inductive Option (A : Type)
       | some A
     def test => some 114514
     """;
 
   @Language("Aya") String dontTestUnsolvedMetaLit = """
     open import arith::Nat
-    open data Nat2 | OO | SS Nat2
-    open data Empty
+    open inductive Nat2 | OO | SS Nat2
+    open inductive Empty
     
     def take Empty => Empty
     def test => take 114514
@@ -50,7 +50,7 @@ example def test4 (A B : Type) (x : A) (y : B) =>
 
   @Language("Aya") String testNorell = """
     open import arith::Nat
-    data Empty
+    inductive Empty
     def Neg (T : Type) => T -> Empty
     // Ulf's counterexample
     def test
@@ -67,9 +67,9 @@ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
     """;
 
   @Language("Aya") String testLiteralAmbiguous3 = """
-    open data List (A : Type) | nil | cons A (List A)
-    open data List2 (A : Type) | nil2 | cons2 A (List2 A)
-    open data Unit | unit
+    open inductive List (A : Type) | nil | cons A (List A)
+    open inductive List2 (A : Type) | nil2 | cons2 A (List2 A)
+    open inductive Unit | unit
     
     def good : List Unit => [ ]
     def bad => [ unit ]
diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/OperatorError.java b/cli-impl/src/test/java/org/aya/test/fixtures/OperatorError.java
index 0524b293d..7c03f0bc0 100644
--- a/cli-impl/src/test/java/org/aya/test/fixtures/OperatorError.java
+++ b/cli-impl/src/test/java/org/aya/test/fixtures/OperatorError.java
@@ -6,7 +6,7 @@
 
 public interface OperatorError {
   @Language("Aya") String testAmbiguous = """
-    open data Nat | zero | suc Nat
+    open inductive Nat | zero | suc Nat
     // Do not replace with the library definition, we need our own fixity
     def infix + (a b: Nat) : Nat => 0
     def infix == (a b: Nat) : Nat => 0
@@ -22,13 +22,13 @@ public interface OperatorError {
     """;
 
   @Language("Aya") String testIssue677 = """
-    data False
+    inductive False
     def fixl ¬ (A : Type) => A -> False
     def NonEmpty (A : Type) => ¬ ¬ A
     """;
 
   @Language("Aya") String testNoAssoc = """
-    open data Nat | zero | suc Nat
+    open inductive Nat | zero | suc Nat
     // Do not replace with the library definition, we need our own fixity
     def infixl + (a b: Nat) => 0
     def infixr ^ (a b : Nat) => 0
@@ -46,7 +46,7 @@ def NonEmpty (A : Type) => ¬ ¬ A
 
   // This should pass
   @Language("Aya") String testModuleImportRename = """
-    open data Nat | zero | suc Nat
+    open inductive Nat | zero | suc Nat
     module A {
       def infixl + (a b: Nat) => 0
     }
diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/PatCohError.java b/cli-impl/src/test/java/org/aya/test/fixtures/PatCohError.java
index d996a01a5..b34b33f63 100644
--- a/cli-impl/src/test/java/org/aya/test/fixtures/PatCohError.java
+++ b/cli-impl/src/test/java/org/aya/test/fixtures/PatCohError.java
@@ -8,7 +8,7 @@
 public interface PatCohError {
   @Language("Aya") String testUnsureMissing = """
     open import arith::Nat
-    open data Fin+1 (n : Nat) : Type
+    open inductive Fin+1 (n : Nat) : Type
     | m => fzero
     | suc m => fsuc (Fin+1 m)
     
@@ -136,7 +136,7 @@ def cov (x x' x'' x''' : Nat) : Nat
   @Language("Aya") String testIApplyConflReduce = """
     open import arith::Nat
     open import Paths
-    open data WrongInt
+    open inductive WrongInt
     | pos Nat
     | neg Nat
     | posneg (n : Nat) : pos n = neg n
diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java b/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java
index 270d19ad1..3ba4a2349 100644
--- a/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java
+++ b/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java
@@ -8,8 +8,8 @@
 public interface PatTyckError {
   // Issue2 746
   @Language("Aya") String testUnknownCon = """
-    open data Test1 | test1
-    open data Test2 | test2
+    open inductive Test1 | test1
+    open inductive Test2 | test2
     
     def test Test1 : Test1
     | test2 => test1
@@ -31,13 +31,13 @@ public interface PatTyckError {
     """;
 
   @Language("Aya") String testSplitOnNonData = """
-    open data Unit | unit
+    open inductive Unit | unit
     def test (a : Type) : Type
      | unit y => a
     """;
 
   @Language("Aya") String testBadLiteral = """
-    open data Test | t
+    open inductive Test | t
     def not-conf Test : Test
     | 1 => t
     """;
@@ -83,13 +83,13 @@ def funExt (f g : A -> B) (p : forall a -> f a = g a) : f = g
     """;
 
   @Language("Aya") String testNewRepoIssue597 = """
-    open data Nat | O | S Nat
+    open inductive Nat | O | S Nat
     def bad Nat : Nat | S S O => O | _ => O
     """;
 
   @Language("Aya") String testNewRepoIssue746 = """
-    open data Test1 | test1
-    open data Test2 | test2
+    open inductive Test1 | test1
+    open inductive Test2 | test2
     def test Test1 : Test1
     | test2 => test1
     """;
diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/ScopeError.java b/cli-impl/src/test/java/org/aya/test/fixtures/ScopeError.java
index 566a827ed..21619a4f9 100644
--- a/cli-impl/src/test/java/org/aya/test/fixtures/ScopeError.java
+++ b/cli-impl/src/test/java/org/aya/test/fixtures/ScopeError.java
@@ -7,12 +7,12 @@
 @SuppressWarnings("unused")
 public interface ScopeError {
   @Language("Aya") String testDidYouMeanDisamb = """
-    open data Nat1 | zero
-    open data Nat2 | zero
+    open inductive Nat1 | zero
+    open inductive Nat2 | zero
     def one => zero
     """;
   @Language("Aya") String testDidYouMean = """
-    data Nat | zero | suc Nat
+    inductive Nat | zero | suc Nat
     def one => suc zero
     """;
   @Language("Aya") String testImportDefineShadow = """
@@ -34,27 +34,27 @@ open A hiding (foo)
     open A hiding (bar)
     """;
   @Language("Aya") String testImportDefineShadow2 = """
-    open data Bool | true | false
+    open inductive Bool | true | false
     module A { def foo => true }
     def foo => false
     open A
     """;
   @Language("Aya") String testInfRec = "def undefined => undefined";
   @Language("Aya") String testIssue247 = """
-    data Z : Type
+    inductive Z : Type
     | zero
     | zero
     """;
   @Language("Aya") String testRedefPrim = "prim I prim I";
   @Language("Aya") String testUnknownPrim = "prim senpaiSuki";
   @Language("Aya") String testUnknownVar = """
-    open data Nat : Type | zero
+    open inductive Nat : Type | zero
     def p => Nat::suc Nat::zero
     """;
   // This should pass
   @Language("Aya") String testLetOpen = """
     open import Paths using (=, refl)
-    data Nat | O | S Nat
+    inductive Nat | O | S Nat
     def zero : Nat => let open Nat using (O) in O
     def suc (n : Nat) : Nat => let open Nat hiding (O) in S n
     def they-are : suc zero = Nat::S Nat::O => refl
diff --git a/cli-impl/src/test/java/org/aya/test/literate/HighlighterTest.java b/cli-impl/src/test/java/org/aya/test/literate/HighlighterTest.java
index 4e1baa828..ecda424eb 100644
--- a/cli-impl/src/test/java/org/aya/test/literate/HighlighterTest.java
+++ b/cli-impl/src/test/java/org/aya/test/literate/HighlighterTest.java
@@ -12,7 +12,7 @@
 public class HighlighterTest {
   @Test public void commonTests() {
     @Language("Aya") String code = """
-      open data Nat
+      open inductive Nat
       | O | S Nat
       
       def add Nat Nat : Nat
@@ -20,37 +20,37 @@ public class HighlighterTest {
       | S n, m => S (add n m)
       """;
 
-    highlightAndTest(code,
+    highlightAndTest("open inductive Nat\n| O | S Nat\n\ndef add Nat Nat : Nat\n| n, 0 => n\n| S n, m => S (add n m)\n",
       keyword(0, 3, "open"),
       whatever(),
-      def(10, 12, "Nat", "nat", HighlightInfo.DefKind.Data),
+      def(15, 17, "Nat", "nat", HighlightInfo.DefKind.Data),
       whatever(), // |
-      def(16, 16, "O", "zero", HighlightInfo.DefKind.Con),
+      def(21, 21, "O", "zero", HighlightInfo.DefKind.Con),
       whatever(), // |
-      def(20, 20, "S", "suc", HighlightInfo.DefKind.Con),
-      ref(22, 24, "Nat", "nat", HighlightInfo.DefKind.Data),
+      def(25, 25, "S", "suc", HighlightInfo.DefKind.Con),
+      ref(27, 29, "Nat", "nat", HighlightInfo.DefKind.Data),
       whatever(),   // def
-      def(31, 33, "add", HighlightInfo.DefKind.Fn),
-      ref(35, 37, "Nat", "nat", HighlightInfo.DefKind.Data),
-      ref(39, 41, "Nat", "nat", HighlightInfo.DefKind.Data),
+      def(36, 38, "add", HighlightInfo.DefKind.Fn),
+      ref(40, 42, "Nat", "nat", HighlightInfo.DefKind.Data),
+      ref(44, 46, "Nat", "nat", HighlightInfo.DefKind.Data),
       whatever(), // :
-      ref(45, 47, "Nat", "nat", HighlightInfo.DefKind.Data),
+      ref(50, 52, "Nat", "nat", HighlightInfo.DefKind.Data),
       whatever(), // |
-      localDef(51, 51, "n", "n'"),
-      litInt(54, 54, 0),
+      localDef(56, 56, "n", "n'"),
+      litInt(59, 59, 0),
       whatever(), // =>
-      localRef(59, 59, "n", "n'"),
+      localRef(64, 64, "n", "n'"),
       whatever(), // |
-      ref(63, 63, "S", "suc", HighlightInfo.DefKind.Con),
+      ref(68, 68, "S", "suc", HighlightInfo.DefKind.Con),
       // Note: n' is still available here, so use another name
-      localDef(65, 65, "n", "n''"),
-      localDef(68, 68, "m", "m'"),
+      localDef(70, 70, "n", "n''"),
+      localDef(73, 73, "m", "m'"),
       whatever(), // =>
-      ref(73, 73, "S", "suc", HighlightInfo.DefKind.Con),
+      ref(78, 78, "S", "suc", HighlightInfo.DefKind.Con),
       whatever(), // (
-      ref(76, 78, "add", HighlightInfo.DefKind.Fn),
-      localRef(80, 80, "n", "n''"),
-      localRef(82, 82, "m", "m'"),
+      ref(81, 83, "add", HighlightInfo.DefKind.Fn),
+      localRef(85, 85, "n", "n''"),
+      localRef(87, 87, "m", "m'"),
       whatever() // )
     );
   }
@@ -58,33 +58,33 @@ public class HighlighterTest {
   @Test public void unformatTest() {
     @Language("Aya") String code = """
          open
-      data  Nat |
+      inductive  Nat |
       O | S Nat
       """;
 
-    highlightAndTest(code,
+    highlightAndTest("   open\ninductive  Nat |\nO | S Nat\n",
       keyword(3, 6, "open"),
-      keyword(8, 11, "data"),
-      def(14, 16, "Nat", "nat", HighlightInfo.DefKind.Data),
+      keyword(8, 16, "inductive"),
+      def(19, 21, "Nat", "nat", HighlightInfo.DefKind.Data),
       whatever(),
-      def(20, 20, "O", HighlightInfo.DefKind.Con),
+      def(25, 25, "O", HighlightInfo.DefKind.Con),
       whatever(),
-      def(24, 24, "S", HighlightInfo.DefKind.Con),
-      ref(26, 28, "Nat", "nat", HighlightInfo.DefKind.Data));
+      def(29, 29, "S", HighlightInfo.DefKind.Con),
+      ref(31, 33, "Nat", "nat", HighlightInfo.DefKind.Data));
   }
 
   @Test public void incorrectTest() {
     assertThrows(Throwable.class, () -> {
       @Language("Aya") String code = """
-        open data List (A : Type)
+        open inductive List (A : Type)
         | nil
         | cons A (List A)
         """;
 
-      highlightAndTest(code,
+      highlightAndTest("open inductive List (A : Type)\n| nil\n| cons A (List A)\n",
         whatever(),
         whatever(),
-        def(10, 13, "L1st", "list", HighlightInfo.DefKind.Data));
+        def(15, 18, "L1st", "list", HighlightInfo.DefKind.Data));
     });
   }
 
@@ -92,7 +92,7 @@ open data List (A : Type)
     @Language("Aya") String code = """
       module X {}
       open X
-      open data Y
+      open inductive Y
       """;
 
     // TODO: enable this test when `SyntaxHighlight.foldModuleRef` is fixed
@@ -109,47 +109,47 @@ open data List (A : Type)
 
   @Test public void params() {
     @Language("Aya") String code = """
-      open data Either (A B : Type)
+      open inductive Either (A B : Type)
       | Left A
       | Right B
       
       def constA {A : Type} (a b : A) : A => a
       """;
 
-    highlightAndTest(code,
+    highlightAndTest("open inductive Either (A B : Type)\n| Left A\n| Right B\n\ndef constA {A : Type} (a b : A) : A => a\n",
       keyword(0, 3, "open"),
-      keyword(5, 8, "data"),
-      def(10, 15, "Either", "DefEither", HighlightInfo.DefKind.Data),
+      keyword(5, 13, "inductive"),
+      def(15, 20, "Either", "DefEither", HighlightInfo.DefKind.Data),
       whatever(), // (
-      localDef(18, 18, "A", "LocalA"),
-      localDef(20, 20, "B", "LocalB"),
+      localDef(23, 23, "A", "LocalA"),
+      localDef(25, 25, "B", "LocalB"),
       whatever(), // :
-      keyword(24, 27, "Type"),
+      keyword(29, 32, "Type"),
       whatever(), // )
       whatever(), // |
-      def(32, 35, "Left", HighlightInfo.DefKind.Con),
-      localRef(37, 37, "A", "LocalA"),
+      def(37, 40, "Left", HighlightInfo.DefKind.Con),
+      localRef(42, 42, "A", "LocalA"),
       whatever(), // |
-      def(41, 45, "Right", HighlightInfo.DefKind.Con),
-      localRef(47, 47, "B", "LocalB"),
+      def(46, 50, "Right", HighlightInfo.DefKind.Con),
+      localRef(52, 52, "B", "LocalB"),
 
-      keyword(50, 52, "def"),
-      def(54, 59, "constA", HighlightInfo.DefKind.Fn),
+      keyword(55, 57, "def"),
+      def(59, 64, "constA", HighlightInfo.DefKind.Fn),
       whatever(), // {
-      localDef(62, 62, "A", "LocalA'"),
+      localDef(67, 67, "A", "LocalA'"),
       whatever(), // :
-      keyword(66, 69, "Type"),
+      keyword(71, 74, "Type"),
       whatever(), // }
       whatever(), // (
-      localDef(73, 73, "a", "Locala"),
-      localDef(75, 75, "b"),
+      localDef(78, 78, "a", "Locala"),
+      localDef(80, 80, "b"),
       whatever(), // :
-      localRef(79, 79, "A", "LocalA'"),
+      localRef(84, 84, "A", "LocalA'"),
       whatever(), // )
       whatever(), // :
-      localRef(84, 84, "A", "LocalA'"),
+      localRef(89, 89, "A", "LocalA'"),
       whatever(), // =>
-      localRef(89, 89, "a", "Locala"));
+      localRef(94, 94, "a", "Locala"));
   }
 
   @Test public void variables() {
@@ -159,7 +159,7 @@ open data Either (A B : Type)
       def id (a : A) : A => a
       """;
 
-    highlightAndTest(code,
+    highlightAndTest("variable A : Type\n\ndef id (a : A) : A => a\n",
       keyword(0, 7, "variable"),
       def(9, 9, "A", "GA", HighlightInfo.DefKind.Generalized),
       whatever(), // :
diff --git a/cli-impl/src/test/resources/literate/compiler-output.aya.md b/cli-impl/src/test/resources/literate/compiler-output.aya.md
index f6db4a7af..830ead289 100644
--- a/cli-impl/src/test/resources/literate/compiler-output.aya.md
+++ b/cli-impl/src/test/resources/literate/compiler-output.aya.md
@@ -16,7 +16,7 @@ def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) idp
 The natural number ($\mathbb{N}$):
 
 ```aya
-open data Nat | zero | suc Nat
+open inductive Nat | zero | suc Nat
 overlap def infixl + Nat Nat : Nat
 | 0, a => a
 | a, 0 => a
@@ -48,7 +48,7 @@ module Yes {
 ### Early type aliases
 
 ```aya
-open data SetTrunc (A : Type)
+open inductive SetTrunc (A : Type)
 | inj A
 //| trunc : isSet (SetTrunc A)
 ```
@@ -58,7 +58,7 @@ def FMSet (A : Type) : Type => SetTrunc (FMSetRaw A)
 ```
 
 ```aya
-open data FMSetRaw (A : Type)
+open inductive FMSetRaw (A : Type)
 | nil
 | infixr :< A (FMSet A)
   tighter =
diff --git a/cli-impl/src/test/resources/literate/expected-test.aya b/cli-impl/src/test/resources/literate/expected-test.aya
index cd2c50403..34289099b 100644
--- a/cli-impl/src/test/resources/literate/expected-test.aya
+++ b/cli-impl/src/test/resources/literate/expected-test.aya
@@ -1,5 +1,5 @@
       
-open data Unit | unit
+open inductive Unit | unit
    
 
                                                                     
@@ -27,7 +27,7 @@ def foo =>
                                                        
 
       
-open data Bool | true | false
+open inductive Bool | true | false
 
 def > (lhs rhs : Unit) : Bool =>
    
diff --git a/cli-impl/src/test/resources/literate/expected-wow.aya b/cli-impl/src/test/resources/literate/expected-wow.aya
index 4ac723477..9fa566501 100644
--- a/cli-impl/src/test/resources/literate/expected-wow.aya
+++ b/cli-impl/src/test/resources/literate/expected-wow.aya
@@ -1,8 +1,8 @@
                          
 
       
-open data Nat | zero | suc Nat
-open data Unit | unit
+open inductive Nat | zero | suc Nat
+open inductive Unit | unit
    
 
                                                                                      
@@ -15,7 +15,7 @@ def wow-fun {U : Type} {T : U -> Type} (A B : U) (x : T A) (y : T B) : Nat => ze
                                                                                
 
       
-open data Wow : Type 2
+open inductive Wow : Type 2
 | wow {U : Type 1} {T : U -> Type} (A B : U) (x : T A) (y : T B)
    
 
diff --git a/cli-impl/src/test/resources/literate/test.aya.md b/cli-impl/src/test/resources/literate/test.aya.md
index 44d2e6ec6..f1ab667db 100644
--- a/cli-impl/src/test/resources/literate/test.aya.md
+++ b/cli-impl/src/test/resources/literate/test.aya.md
@@ -1,5 +1,5 @@
 ```aya
-open data Unit | unit
+open inductive Unit | unit
 ```
 
 This is a tutorial about aya, but I won't tell you how to write aya.
@@ -27,7 +27,7 @@ Umm, now it looks good!
 Also, we can use some special characters as identifier:
 
 ```aya
-open data Bool | true | false
+open inductive Bool | true | false
 
 def > (lhs rhs : Unit) : Bool =>
 ```
diff --git a/cli-impl/src/test/resources/literate/wow.aya.md b/cli-impl/src/test/resources/literate/wow.aya.md
index c02b09685..af0f072e1 100644
--- a/cli-impl/src/test/resources/literate/wow.aya.md
+++ b/cli-impl/src/test/resources/literate/wow.aya.md
@@ -1,8 +1,8 @@
 Some preload definitions:
 
 ```aya
-open data Nat | zero | suc Nat
-open data Unit | unit
+open inductive Nat | zero | suc Nat
+open inductive Unit | unit
 ```
 
 Lately, **Daylily** told me an interesting problem about Aya's _pattern unification_.
@@ -15,7 +15,7 @@ def wow-fun {U : Type} {T : U -> Type} (A B : U) (x : T A) (y : T B) : Nat => ze
 In order to make it irreducible, we make it a constructor of an inductive type:
 
 ```aya
-open data Wow : Type 2
+open inductive Wow : Type 2
 | wow {U : Type 1} {T : U -> Type} (A B : U) (x : T A) (y : T B)
 ```
 
diff --git a/cli-impl/src/test/resources/negative/ExprTyckError.txt b/cli-impl/src/test/resources/negative/ExprTyckError.txt
index ee28fe28d..284b64648 100644
--- a/cli-impl/src/test/resources/negative/ExprTyckError.txt
+++ b/cli-impl/src/test/resources/negative/ExprTyckError.txt
@@ -110,11 +110,11 @@ Error: `prim Path` is expected to have a return type
 What are you doing?
 
 PiDom:
-In file $FILE:2:23 ->
+In file $FILE:2:28 ->
 
-  1 │   data X : Set
-  2 │   data Test : Type | con X
-    │                          ╰╯
+  1 │   inductive X : Set
+  2 │   inductive Test : Type | con X
+    │                               ╰╯
 
 Error: The type
          X
@@ -127,8 +127,8 @@ What are you doing?
 PiDomMeta:
 In file $FILE:4:19 ->
 
-  2 │   data infix = (a b : X) : Type
-  3 │   data Test : Type
+  2 │   inductive infix = (a b : X) : Type
+  3 │   inductive Test : Type
   4 │   | con (x : _) (y : X) (x = y)
     │                      ╰╯
 
@@ -139,8 +139,8 @@ Error: The type
 
 In file $FILE:4:11 ->
 
-  2 │   data infix = (a b : X) : Type
-  3 │   data Test : Type
+  2 │   inductive infix = (a b : X) : Type
+  3 │   inductive Test : Type
   4 │   | con (x : _) (y : X) (x = y)
     │              ╰╯
 
diff --git a/cli-impl/src/test/resources/negative/GoalAndMeta.txt b/cli-impl/src/test/resources/negative/GoalAndMeta.txt
index cc940e46b..b1ffcc5d9 100644
--- a/cli-impl/src/test/resources/negative/GoalAndMeta.txt
+++ b/cli-impl/src/test/resources/negative/GoalAndMeta.txt
@@ -37,7 +37,7 @@ What are you doing?
 UnsolvedMetaLit:
 In file $FILE:5:17 ->
 
-  3 │   open data Option (A : Type)
+  3 │   open inductive Option (A : Type)
   4 │     | some A
   5 │   def test => some 114514
     │                    ╰────╯
@@ -47,7 +47,7 @@ Error: Unsolved meta A
 
 In file $FILE:5:17 ->
 
-  3 │   open data Option (A : Type)
+  3 │   open inductive Option (A : Type)
   4 │     | some A
   5 │   def test => some 114514
     │                    ╰────╯
@@ -57,7 +57,7 @@ Error: Unsolved meta A
 
 In file $FILE:5:17 ->
 
-  3 │   open data Option (A : Type)
+  3 │   open inductive Option (A : Type)
   4 │     | some A
   5 │   def test => some 114514
     │                    ╰────╯
diff --git a/cli-impl/src/test/resources/negative/OperatorError.txt b/cli-impl/src/test/resources/negative/OperatorError.txt
index a80a91d9a..11ea43f16 100644
--- a/cli-impl/src/test/resources/negative/OperatorError.txt
+++ b/cli-impl/src/test/resources/negative/OperatorError.txt
@@ -29,7 +29,7 @@ What are you doing?
 Issue677:
 In file $FILE:3:27 ->
 
-  1 │   data False
+  1 │   inductive False
   2 │   def fixl ¬ (A : Type) => A -> False
   3 │   def NonEmpty (A : Type) => ¬ ¬ A
     │                              ╰╯
@@ -38,7 +38,7 @@ Error: There is no operand for this operator `¬`
 
 In file $FILE:3:4 ->
 
-  1 │   data False
+  1 │   inductive False
   2 │   def fixl ¬ (A : Type) => A -> False
   3 │   def NonEmpty (A : Type) => ¬ ¬ A
     │       ╰──────╯
diff --git a/cli-impl/src/test/resources/negative/PatTyckError.txt b/cli-impl/src/test/resources/negative/PatTyckError.txt
index dec7b0da2..b2d0924e6 100644
--- a/cli-impl/src/test/resources/negative/PatTyckError.txt
+++ b/cli-impl/src/test/resources/negative/PatTyckError.txt
@@ -13,109 +13,52 @@ Error: Unknown constructor
 What are you doing?
 
 SelectionFailed:
-In file $FILE:2:4 ->
-
-  1 │   open import arith::Nat
-  2 │   open import data::Vec
-    │       ╰╯
-  3 │   def mapImpl {A B : Type} {n : Nat} (f : A -> B) (xs : Vec (n + n) A) : Vec (n + n) B elim xs
-
-Error: Cannot parse
-
-In file $FILE:2:11 ->
-
-  1 │   open import arith::Nat
-  2 │   open import data::Vec
-    │              ╰╯
-  3 │   def mapImpl {A B : Type} {n : Nat} (f : A -> B) (xs : Vec (n + n) A) : Vec (n + n) B elim xs
-
-Error: Cannot parse
-
-In file $FILE:2:16 ->
-
-  1 │   open import arith::Nat
-  2 │   open import data::Vec
-    │                   ╰╯
-  3 │   def mapImpl {A B : Type} {n : Nat} (f : A -> B) (xs : Vec (n + n) A) : Vec (n + n) B elim xs
-
-Error: Cannot parse
-
-In file $FILE:2:12 ->
+In file $FILE:4:2 ->
 
-  1 │   open import arith::Nat
   2 │   open import data::Vec
-    │               ╰──╯
   3 │   def mapImpl {A B : Type} {n : Nat} (f : A -> B) (xs : Vec (n + n) A) : Vec (n + n) B elim xs
+  4 │   | [] => []
+    │     ╰╯
 
-Error: Expect a name
+Error: I'm unsure if there should be a case for
+         []
+       as index unification is blocked for type
+         Vec (<n> + <n>) A
 
-In file $FILE:3:54 ->
+In file $FILE:5:2 ->
 
-  1 │   open import arith::Nat
-  2 │   open import data::Vec
   3 │   def mapImpl {A B : Type} {n : Nat} (f : A -> B) (xs : Vec (n + n) A) : Vec (n + n) B elim xs
-    │                                                         ╰─╯
+  4 │   | [] => []
+  5 │   | _ :> _ => _
+    │     ╰────╯
 
-Error: The name `Vec` is not defined in the current scope
+Error: I'm unsure if there should be a case for
+         :> _ _
+       as index unification is blocked for type
+         Vec (<n> + <n>) A
 
-Resolving interrupted due to:
-5 error(s), 0 warning(s).
+2 error(s), 0 warning(s).
 What are you doing?
 
 SelectionBlocked:
-In file $FILE:2:4 ->
-
-  1 │   open import arith::Nat
-  2 │   open import data::Vec
-    │       ╰╯
-  3 │   def mapImpl {A B : Type} {n : Nat} (f : A -> B) (xs : Vec (n + n) A) : Vec (n + n) B elim xs
-
-Error: Cannot parse
-
-In file $FILE:2:11 ->
-
-  1 │   open import arith::Nat
-  2 │   open import data::Vec
-    │              ╰╯
-  3 │   def mapImpl {A B : Type} {n : Nat} (f : A -> B) (xs : Vec (n + n) A) : Vec (n + n) B elim xs
-
-Error: Cannot parse
-
-In file $FILE:2:16 ->
-
-  1 │   open import arith::Nat
-  2 │   open import data::Vec
-    │                   ╰╯
-  3 │   def mapImpl {A B : Type} {n : Nat} (f : A -> B) (xs : Vec (n + n) A) : Vec (n + n) B elim xs
-
-Error: Cannot parse
-
-In file $FILE:2:12 ->
-
-  1 │   open import arith::Nat
-  2 │   open import data::Vec
-    │               ╰──╯
-  3 │   def mapImpl {A B : Type} {n : Nat} (f : A -> B) (xs : Vec (n + n) A) : Vec (n + n) B elim xs
-
-Error: Expect a name
-
-In file $FILE:3:54 ->
+In file $FILE:4:2 ->
 
-  1 │   open import arith::Nat
   2 │   open import data::Vec
   3 │   def mapImpl {A B : Type} {n : Nat} (f : A -> B) (xs : Vec (n + n) A) : Vec (n + n) B elim xs
-    │                                                         ╰─╯
+  4 │   | () => []
+    │     ╰╯
 
-Error: The name `Vec` is not defined in the current scope
+Error: Unsure if this pattern is actually impossible, as constructor selection 
+       is blocked on:
+         Vec (<n> + <n>) A
 
-Resolving interrupted due to:
-5 error(s), 0 warning(s).
+1 error(s), 0 warning(s).
 What are you doing?
 
 SplitOnNonData:
 In file $FILE:3:3 ->
 
-  1 │   open data Unit | unit
+  1 │   open inductive Unit | unit
   2 │   def test (a : Type) : Type
   3 │    | unit y => a
     │      ╰────╯
@@ -131,7 +74,7 @@ What are you doing?
 BadLiteral:
 In file $FILE:3:2 ->
 
-  1 │   open data Test | t
+  1 │   open inductive Test | t
   2 │   def not-conf Test : Test
   3 │   | 1 => t
     │     ╰╯
@@ -244,7 +187,7 @@ What are you doing?
 NewRepoIssue597:
 In file $FILE:2:22 ->
 
-  1 │   open data Nat | O | S Nat
+  1 │   open inductive Nat | O | S Nat
   2 │   def bad Nat : Nat | S S O => O | _ => O
     │                         ╰╯
 
@@ -253,7 +196,7 @@ Error: There is no pattern for the parameter
 
 In file $FILE:2:24 ->
 
-  1 │   open data Nat | O | S Nat
+  1 │   open inductive Nat | O | S Nat
   2 │   def bad Nat : Nat | S S O => O | _ => O
     │                           ╰╯
 
@@ -269,7 +212,7 @@ What are you doing?
 NewRepoIssue746:
 In file $FILE:4:2 ->
 
-  2 │   open data Test2 | test2
+  2 │   open inductive Test2 | test2
   3 │   def test Test1 : Test1
   4 │   | test2 => test1
     │     ╰───╯
diff --git a/cli-impl/src/test/resources/negative/ScopeError.txt b/cli-impl/src/test/resources/negative/ScopeError.txt
index 90f4afb6d..4dd243ac2 100644
--- a/cli-impl/src/test/resources/negative/ScopeError.txt
+++ b/cli-impl/src/test/resources/negative/ScopeError.txt
@@ -1,17 +1,17 @@
 DidYouMeanDisamb:
-In file $FILE:2:17 ->
+In file $FILE:2:22 ->
 
-  1 │   open data Nat1 | zero
-  2 │   open data Nat2 | zero
-    │                    ╰──╯
+  1 │   open inductive Nat1 | zero
+  2 │   open inductive Nat2 | zero
+    │                         ╰──╯
   3 │   def one => zero
 
 Warning: The name `zero` shadows a previous local definition from outer scope
 
 In file $FILE:2:0 ->
 
-  1 │   open data Nat1 | zero
-  2 │   open data Nat2 | zero
+  1 │   open inductive Nat1 | zero
+  2 │   open inductive Nat2 | zero
     │   ╰──╯
   3 │   def one => zero
 
@@ -20,8 +20,8 @@ Warning: The name `zero` introduces ambiguity and can only be accessed through a
 
 In file $FILE:3:11 ->
 
-  1 │   open data Nat1 | zero
-  2 │   open data Nat2 | zero
+  1 │   open inductive Nat1 | zero
+  2 │   open inductive Nat2 | zero
   3 │   def one => zero
     │              ╰──╯
 
@@ -37,7 +37,7 @@ What are you doing?
 DidYouMean:
 In file $FILE:2:11 ->
 
-  1 │   data Nat | zero | suc Nat
+  1 │   inductive Nat | zero | suc Nat
   2 │   def one => suc zero
     │              ╰─╯
 
@@ -116,7 +116,7 @@ What are you doing?
 Issue247:
 In file $FILE:3:2 ->
 
-  1 │   data Z : Type
+  1 │   inductive Z : Type
   2 │   | zero
   3 │   | zero
     │     ╰──╯
@@ -154,7 +154,7 @@ What are you doing?
 UnknownVar:
 In file $FILE:2:9 ->
 
-  1 │   open data Nat : Type | zero
+  1 │   open inductive Nat : Type | zero
   2 │   def p => Nat::suc Nat::zero
     │            ╰──────╯
 
diff --git a/cli-impl/src/test/resources/shared/src/arith/Bool.aya b/cli-impl/src/test/resources/shared/src/arith/Bool.aya
index 12e94aadb..aba147e6c 100644
--- a/cli-impl/src/test/resources/shared/src/arith/Bool.aya
+++ b/cli-impl/src/test/resources/shared/src/arith/Bool.aya
@@ -1,4 +1,4 @@
-open data Bool | true | false
+open inductive Bool | true | false
 def not Bool : Bool
 | true => false
 | false => true
diff --git a/cli-impl/src/test/resources/shared/src/arith/Int.aya b/cli-impl/src/test/resources/shared/src/arith/Int.aya
index 854bf282b..2aca59426 100644
--- a/cli-impl/src/test/resources/shared/src/arith/Int.aya
+++ b/cli-impl/src/test/resources/shared/src/arith/Int.aya
@@ -1,7 +1,7 @@
 open import arith::Nat
 open import arith::Bool
 open import Paths
-open data Int
+open inductive Int
 | signed Bool Nat
 | posneg : neg 0 = pos 0
 
diff --git a/cli-impl/src/test/resources/shared/src/arith/Nat.aya b/cli-impl/src/test/resources/shared/src/arith/Nat.aya
index 50e37390e..4cf9300da 100644
--- a/cli-impl/src/test/resources/shared/src/arith/Nat.aya
+++ b/cli-impl/src/test/resources/shared/src/arith/Nat.aya
@@ -1,6 +1,6 @@
 open import Paths
 
-open data Nat | zero | suc Nat
+open inductive Nat | zero | suc Nat
 
 overlap def infixl + Nat Nat : Nat
 | 0, b => b
diff --git a/cli-impl/src/test/resources/shared/src/data/Interval.aya b/cli-impl/src/test/resources/shared/src/data/Interval.aya
index 4d8ef610c..b7fb7d83b 100644
--- a/cli-impl/src/test/resources/shared/src/data/Interval.aya
+++ b/cli-impl/src/test/resources/shared/src/data/Interval.aya
@@ -1,6 +1,6 @@
 open import Paths
 
-open data Interval
+open inductive Interval
 | left
 | right
 | line : left = right
diff --git a/cli-impl/src/test/resources/shared/src/data/Vec.aya b/cli-impl/src/test/resources/shared/src/data/Vec.aya
index f6b9d299c..7d1785bce 100644
--- a/cli-impl/src/test/resources/shared/src/data/Vec.aya
+++ b/cli-impl/src/test/resources/shared/src/data/Vec.aya
@@ -1,7 +1,7 @@
 open import arith::Nat
 open import Paths
 
-open data Vec Nat Type
+open inductive Vec Nat Type
 | 0, A => []
 | suc n, A => infixr :> A (Vec n A)
 
diff --git a/cli-impl/src/test/resources/shared/src/type-theory/Thorsten.aya b/cli-impl/src/test/resources/shared/src/type-theory/Thorsten.aya
index f6fea6599..099a1b4cc 100644
--- a/cli-impl/src/test/resources/shared/src/type-theory/Thorsten.aya
+++ b/cli-impl/src/test/resources/shared/src/type-theory/Thorsten.aya
@@ -1,6 +1,6 @@
 open import Paths
 
-open data Con : Type
+open inductive Con : Type
 | •
 | infix ▷ (Γ : Con) (Ty Γ)
 
@@ -9,7 +9,7 @@ open data Con : Type
 //  δ ∘ π₁ (id refl) ∷ transport (Tm _) SubAss (π₂ (id refl))
 
 // Incomplete
-open data Ty (Γ : Con) : Type
+open inductive Ty (Γ : Con) : Type
 | U
 | Π (A : Ty Γ) (B : Ty (Γ ▷ A))
 | El (A : Tm Γ U)
@@ -24,7 +24,7 @@ open data Ty (Γ : Con) : Type
 //    : Subst (Π A B) σ = Π (Subst A σ) (Subst B (ext σ A))
 
 // Tms
-open data infix << (Γ : Con) (Δ : Con) : Type
+open inductive infix << (Γ : Con) (Δ : Con) : Type
    tighter = looser ▷
 | _, • => ε
 | _, Δ' ▷ A => infixr ∷ (δ : Γ << Δ') (Tm Γ (Subst A δ)) tighter =
@@ -42,7 +42,7 @@ open data infix << (Γ : Con) (Δ : Con) : Type
 | _, • => εη {δ : Γ << •} : δ = ε
 
 // Incomplete
-open data Tm (Γ : Con) (A : Ty Γ) : Type
+open inductive Tm (Γ : Con) (A : Ty Γ) : Type
 | _, Π A' B => λ (Tm (Γ ▷ A') B)
 | Γ' ▷ A', B => app (Tm Γ' (Π A' B))
 | _, Subst A' δ => sub (Tm _ A')
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 c5d43ce5c..6f9d6fc04 100644
--- a/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
+++ b/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
@@ -91,18 +91,20 @@ public class LspTest {
 
     var param = new TextDocumentPositionParams(new TextDocumentIdentifier(
       TEST_LIB.resolve("src/Nat/Core.aya").toUri()),
-      new Position(0, 18)
+      new Position(0, 23)
     );
 
     var result0 = client.service.hover(param);
     assertTrue(result0.isPresent());
-    assertEquals("<a href=\"#Nat-Core-Nat\"><span style=\"color:#218c21;\">Nat</span></a>", result0.get().contents.getFirst().value);
+    assertEquals("<a href=\"#Nat-Core-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=\"#Nat-Core-Nat\"><span style=\"color:#000000;\">Nat</span></a>", result1.get().contents.getFirst().value);
+    assertEquals("<a href=\"#Nat-Core-Nat\"><span style=\"color:#000000;\">Nat</span></a>",
+      result1.get().contents.getFirst().value);
   }
 
   private void logTime(long time) {
diff --git a/ide-lsp/src/test/resources/lsp-test-lib/src/Nat/Core.aya b/ide-lsp/src/test/resources/lsp-test-lib/src/Nat/Core.aya
index 60269ce48..def8b7698 100644
--- a/ide-lsp/src/test/resources/lsp-test-lib/src/Nat/Core.aya
+++ b/ide-lsp/src/test/resources/lsp-test-lib/src/Nat/Core.aya
@@ -1 +1 @@
-open data Nat | zero | suc Nat
+open inductive Nat | zero | suc Nat
diff --git a/ide-lsp/src/test/resources/lsp-test-lib/src/VecCore.aya b/ide-lsp/src/test/resources/lsp-test-lib/src/VecCore.aya
index cc0a95b7c..de8a89f08 100644
--- a/ide-lsp/src/test/resources/lsp-test-lib/src/VecCore.aya
+++ b/ide-lsp/src/test/resources/lsp-test-lib/src/VecCore.aya
@@ -1,6 +1,6 @@
 open import Nat::Core
 
-open data Vec Type Nat : Type
+open inductive Vec Type Nat : Type
 | A, 0 => vnil
 | A, suc m => infixr :> A (Vec A m)
 
diff --git a/jit-compiler/src/test/java/CompileTest.java b/jit-compiler/src/test/java/CompileTest.java
index 85a98d9b1..ad9828e49 100644
--- a/jit-compiler/src/test/java/CompileTest.java
+++ b/jit-compiler/src/test/java/CompileTest.java
@@ -35,8 +35,8 @@
 public class CompileTest {
   @Test public void test0() {
     var result = tyck("""
-      open data Nat | O | S Nat
-      open data Vec (n : Nat) Type
+      open inductive Nat | O | S Nat
+      open inductive Vec (n : Nat) Type
       | O, A   => vnil
       | S n, A => vcons A (Vec n A)
       
diff --git a/jit-compiler/src/test/resources/TreeSort.aya b/jit-compiler/src/test/resources/TreeSort.aya
index 86190d49b..a640bd583 100644
--- a/jit-compiler/src/test/resources/TreeSort.aya
+++ b/jit-compiler/src/test/resources/TreeSort.aya
@@ -1,6 +1,6 @@
-open data Nat | O | S Nat
-open data Bool | True | False
-open data List Type
+open inductive Nat | O | S Nat
+open inductive Bool | True | False
+open inductive List Type
 | []
 | A => infixr :> A (List A)
 
@@ -8,12 +8,12 @@ def isZero (a : Nat) : Bool
 | 0 => True
 | _ => False
 
-open data Color | red | black
+open inductive Color | red | black
 def Decider (A : Type) => Fn (x y : A) -> Bool
 
 variable A : Type
 
-open data RBTree (A : Type) : Type
+open inductive RBTree (A : Type) : Type
 | rbLeaf
 | rbNode Color (RBTree A) A (RBTree A)
 
diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java
index 73d31ce00..f6690e17d 100644
--- a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java
+++ b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java
@@ -1,6 +1,3 @@
-// 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.
-
 // This is a generated file. Not intended for manual editing.
 package org.aya.parser;
 
@@ -120,10 +117,10 @@ public interface AyaPsiElementTypes {
   IElementType KW_AS = new AyaPsiTokenType("as");
   IElementType KW_CLASS = new AyaPsiTokenType("class");
   IElementType KW_CLASSIFIYING = new AyaPsiTokenType("classifying");
-  IElementType KW_CODATA = new AyaPsiTokenType("codata");
+  IElementType KW_CODATA = new AyaPsiTokenType("coinductive");
   IElementType KW_COERCE = new AyaPsiTokenType("coerce");
   IElementType KW_COMPLETED = new AyaPsiTokenType("completed");
-  IElementType KW_DATA = new AyaPsiTokenType("data");
+  IElementType KW_DATA = new AyaPsiTokenType("inductive");
   IElementType KW_DEF = new AyaPsiTokenType("def");
   IElementType KW_DO = new AyaPsiTokenType("do");
   IElementType KW_ELIM = new AyaPsiTokenType("elim");
diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
index 7929b00e4..a687d8535 100644
--- a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
+++ b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
@@ -1,6 +1,3 @@
-// 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.
-
 // This is a generated file. Not intended for manual editing.
 package org.aya.parser;
 
diff --git a/parser/src/main/grammar/AyaPsiLexer.flex b/parser/src/main/grammar/AyaPsiLexer.flex
index 6de2d2a41..db9d5dcd1 100644
--- a/parser/src/main/grammar/AyaPsiLexer.flex
+++ b/parser/src/main/grammar/AyaPsiLexer.flex
@@ -132,7 +132,7 @@ BLOCK_COMMENT_END   = "*/"
   "def"                 { return KW_DEF; }
   "class"               { return KW_CLASS; }
   "classifying"         { return KW_CLASSIFIYING; }
-  "data"                { return KW_DATA; }
+  "inductive"           { return KW_DATA; }
   "prim"                { return KW_PRIM; }
   "extends"             { return KW_EXTENDS; }
   "new"                 { return KW_NEW; }
@@ -140,7 +140,7 @@ BLOCK_COMMENT_END   = "*/"
   "self"                { return KW_SELF; }
   "elim"                { return KW_ELIM; }
   "override"            { return KW_OVERRIDE; }
-  "codata"              { return KW_CODATA; }
+  "cocoinductive"       { return KW_CODATA; }
   "let"                 { return KW_LET; }
   "in"                  { return KW_IN; }
   "completed"           { return KW_COMPLETED; }
diff --git a/parser/src/main/grammar/AyaPsiParser.bnf b/parser/src/main/grammar/AyaPsiParser.bnf
index 23421e5fa..6868b3c44 100644
--- a/parser/src/main/grammar/AyaPsiParser.bnf
+++ b/parser/src/main/grammar/AyaPsiParser.bnf
@@ -69,20 +69,20 @@
     KW_VARIABLE = 'variable'
     KW_DEF = 'def'
     KW_CLASS = 'class'
-    KW_CLASSIFIYING = 'classifying'
-    KW_DATA = 'data'
+    KW_DATA = 'inductive'
     KW_PRIM = 'prim'
     KW_EXTENDS = 'extends'
     KW_NEW = 'new'
     KW_DO = 'do'
-    KW_SELF = 'self'
-    KW_OVERRIDE = 'override'
     KW_ELIM = 'elim'
-
-    // Unimplemented but reserved
-    KW_CODATA = 'codata'
     KW_LET = 'let'
     KW_IN = 'in'
+
+    // Unimplemented but reserved
+    KW_CLASSIFIYING = 'classifying'
+    KW_SELF = 'self'
+    KW_OVERRIDE = 'override'
+    KW_CODATA = 'coinductive'
     KW_COMPLETED = 'completed'
 
     // symbols
diff --git a/pretty/src/test/java/org/aya/pretty/MdStyleTest.java b/pretty/src/test/java/org/aya/pretty/MdStyleTest.java
index 10c7c835d..1766c7862 100644
--- a/pretty/src/test/java/org/aya/pretty/MdStyleTest.java
+++ b/pretty/src/test/java/org/aya/pretty/MdStyleTest.java
@@ -16,24 +16,24 @@ public class MdStyleTest {
     assertEquals("""
       # H1
       [Click me](https://google.com)
-            
+      
       ## H2
       ### H3
       #### H4
       ##### H5
       ###### H6
       > BlockQuote
-            
+      
       1\\. fake list
-            
+      
       I love Java.I love Aya.I love Aya's pretty printer.I love Java
-            
+      
       I love Aya
-            
+      
       I love Aya's pretty printer.
-            
+      
       ```aya
-      data Nat | zero | suc Nat
+      inductive Nat | zero | suc Nat
       ```
       Look! She is beautiful
       
@@ -58,7 +58,7 @@ public class MdStyleTest {
       Doc.styled(MdStyle.GFM.Paragraph, "I love Java"),
       Doc.styled(MdStyle.GFM.Paragraph, "I love Aya"),
       Doc.styled(MdStyle.GFM.Paragraph, "I love Aya's pretty printer."),
-      Doc.codeBlock(Language.Builtin.Aya, "data Nat | zero | suc Nat"),
+      Doc.codeBlock(Language.Builtin.Aya, "inductive Nat | zero | suc Nat"),
       Doc.styled(MdStyle.GFM.Paragraph, "Look! She is beautiful")
     );
   }
diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java
index 3707913cf..7c733712e 100644
--- a/producer/src/main/java/org/aya/producer/AyaProducer.java
+++ b/producer/src/main/java/org/aya/producer/AyaProducer.java
@@ -554,7 +554,16 @@ private record DeclNameOrInfix(@NotNull WithPos<String> name, @Nullable OpDecl.O
     //   );
     // }
     if (node.is(ARROW_EXPR)) {
-      var exprs = node.childrenOfType(EXPR);
+      var exprs = node.childrenOfType(EXPR).toImmutableSeq();
+      if (!exprs.sizeEquals(2)) {
+        reporter.report(new ParseError(pos, exprs.joinToString(
+          ",",
+          "In an arrow expr, I see " + exprs.size() + " expr(s): [",
+          "], but I need 2.",
+          GenericNode::tokenText
+        )));
+        throw new ParsingInterruptedException();
+      }
       var expr0 = exprs.get(0);
       var to = expr(exprs.get(1));
       var paramPos = sourcePosOf(expr0);
diff --git a/syntax/src/main/java/org/aya/prettier/Tokens.java b/syntax/src/main/java/org/aya/prettier/Tokens.java
index 790849092..d61d62203 100644
--- a/syntax/src/main/java/org/aya/prettier/Tokens.java
+++ b/syntax/src/main/java/org/aya/prettier/Tokens.java
@@ -37,7 +37,7 @@ private Tokens() {
   public static final Doc KW_LET = Doc.styled(KEYWORD, "let");
   public static final Doc KW_IN = Doc.styled(KEYWORD, "in");
   public static final Doc KW_DEF = Doc.styled(KEYWORD, "def");
-  public static final Doc KW_DATA = Doc.styled(KEYWORD, "data");
+  public static final Doc KW_DATA = Doc.styled(KEYWORD, "inductive");
   public static final Doc PAT_ABSURD = Doc.styled(KEYWORD, "()");
   public static final Doc KW_TIGHTER = Doc.styled(KEYWORD, "tighter");
   public static final Doc KW_LOOSER = Doc.styled(KEYWORD, "looser");