diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean
index 2702889daa..7f9f8f41c9 100644
--- a/src/Lean/Compiler/IR/Basic.lean
+++ b/src/Lean/Compiler/IR/Basic.lean
@@ -406,23 +406,23 @@ inductive Decl where
 namespace Decl
 
 def name : Decl → FunId
-  | Decl.fdecl f ..  => f
-  | Decl.extern f .. => f
+  | .fdecl f ..  => f
+  | .extern f .. => f
 
 def params : Decl → Array Param
-  | Decl.fdecl (xs := xs) ..  => xs
-  | Decl.extern (xs := xs) .. => xs
+  | .fdecl (xs := xs) ..  => xs
+  | .extern (xs := xs) .. => xs
 
 def resultType : Decl → IRType
-  | Decl.fdecl (type := t) ..  => t
-  | Decl.extern (type := t) .. => t
+  | .fdecl (type := t) ..  => t
+  | .extern (type := t) .. => t
 
 def isExtern : Decl → Bool
-  | Decl.extern .. => true
+  | .extern .. => true
   | _ => false
 
 def getInfo : Decl → DeclInfo
-  | Decl.fdecl (info := info) .. => info
+  | .fdecl (info := info) .. => info
   | _ => {}
 
 def updateBody! (d : Decl) (bNew : FnBody) : Decl :=
diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean
index 591a4eb9f3..366bbe413b 100644
--- a/src/Lean/Compiler/IR/Borrow.lean
+++ b/src/Lean/Compiler/IR/Borrow.lean
@@ -90,7 +90,7 @@ partial def visitFnBody (fnid : FunId) : FnBody → StateM ParamMap Unit
 
 def visitDecls (env : Environment) (decls : Array Decl) : StateM ParamMap Unit :=
   decls.forM fun decl => match decl with
-    | Decl.fdecl (f := f) (xs := xs) (body := b) .. => do
+    | .fdecl (f := f) (xs := xs) (body := b) .. => do
       let exported := isExport env f
       modify fun m => m.insert (ParamMap.Key.decl f) (initBorrowIfNotExported exported xs)
       visitFnBody f b
@@ -281,7 +281,7 @@ partial def collectFnBody : FnBody → M Unit
   | e                      => do unless e.isTerminal do collectFnBody e.body
 
 partial def collectDecl : Decl → M Unit
-  | Decl.fdecl (f := f) (xs := ys) (body := b) .. =>
+  | .fdecl (f := f) (xs := ys) (body := b) .. =>
     withReader (fun ctx => let ctx := updateParamSet ctx ys; { ctx with currFn := f }) do
       collectFnBody b
       updateParamMap (ParamMap.Key.decl f)
diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean
index ddddb66e79..fe87373661 100644
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/src/Lean/Compiler/IR/Boxing.lean
@@ -327,7 +327,7 @@ def run (env : Environment) (decls : Array Decl) : Array Decl :=
   let ctx : BoxingContext := { decls := decls, env := env }
   let decls := decls.foldl (init := #[]) fun newDecls decl =>
     match decl with
-    | Decl.fdecl (f := f) (xs := xs) (type := t) (body := b) .. =>
+    | .fdecl (f := f) (xs := xs) (type := t) (body := b) .. =>
       let nextIdx  := decl.maxIndex + 1
       let (b, s)   := (withParams xs (visitFnBody b) { ctx with f := f, resultType := t }).run { nextIdx := nextIdx }
       let newDecls := newDecls ++ s.auxDecls
diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean
index fcd325fba9..0eae0668ef 100644
--- a/src/Lean/Compiler/IR/Checker.lean
+++ b/src/Lean/Compiler/IR/Checker.lean
@@ -146,30 +146,30 @@ def checkExpr (ty : IRType) : Expr → M Unit
   withReader (fun _ => { ctx with localCtx := localCtx }) k
 
 partial def checkFnBody : FnBody → M Unit
-  | FnBody.vdecl x t v b    => do
+  | .vdecl x t v b    => do
     checkExpr t v
     markVar x
     withReader (fun ctx => { ctx with localCtx := ctx.localCtx.addLocal x t v }) (checkFnBody b)
-  | FnBody.jdecl j ys v b => do
+  | .jdecl j ys v b => do
     markJP j
     withParams ys (checkFnBody v)
     withReader (fun ctx => { ctx with localCtx := ctx.localCtx.addJP j ys v }) (checkFnBody b)
-  | FnBody.set x _ y b      => checkVar x *> checkArg y *> checkFnBody b
-  | FnBody.uset x _ y b     => checkVar x *> checkVar y *> checkFnBody b
-  | FnBody.sset x _ _ y _ b => checkVar x *> checkVar y *> checkFnBody b
-  | FnBody.setTag x _ b     => checkVar x *> checkFnBody b
-  | FnBody.inc x _ _ _ b    => checkVar x *> checkFnBody b
-  | FnBody.dec x _ _ _ b    => checkVar x *> checkFnBody b
-  | FnBody.del x b          => checkVar x *> checkFnBody b
-  | FnBody.mdata _ b        => checkFnBody b
-  | FnBody.jmp j ys         => checkJP j *> checkArgs ys
-  | FnBody.ret x            => checkArg x
-  | FnBody.case _ x _ alts  => checkVar x *> alts.forM (fun alt => checkFnBody alt.body)
-  | FnBody.unreachable      => pure ()
+  | .set x _ y b      => checkVar x *> checkArg y *> checkFnBody b
+  | .uset x _ y b     => checkVar x *> checkVar y *> checkFnBody b
+  | .sset x _ _ y _ b => checkVar x *> checkVar y *> checkFnBody b
+  | .setTag x _ b     => checkVar x *> checkFnBody b
+  | .inc x _ _ _ b    => checkVar x *> checkFnBody b
+  | .dec x _ _ _ b    => checkVar x *> checkFnBody b
+  | .del x b          => checkVar x *> checkFnBody b
+  | .mdata _ b        => checkFnBody b
+  | .jmp j ys         => checkJP j *> checkArgs ys
+  | .ret x            => checkArg x
+  | .case _ x _ alts  => checkVar x *> alts.forM (fun alt => checkFnBody alt.body)
+  | .unreachable      => pure ()
 
 def checkDecl : Decl → M Unit
-  | Decl.fdecl (xs := xs) (body := b) .. => withParams xs (checkFnBody b)
-  | Decl.extern (xs := xs) .. => withParams xs (pure ())
+  | .fdecl (xs := xs) (body := b) .. => withParams xs (checkFnBody b)
+  | .extern (xs := xs) .. => withParams xs (pure ())
 
 end Checker
 
diff --git a/src/Lean/Compiler/IR/CompilerM.lean b/src/Lean/Compiler/IR/CompilerM.lean
index e4cecf98f6..7af84f6b6e 100644
--- a/src/Lean/Compiler/IR/CompilerM.lean
+++ b/src/Lean/Compiler/IR/CompilerM.lean
@@ -142,7 +142,7 @@ def getDecl' (n : Name) (decls : Array Decl) : CompilerM Decl := do
 @[export lean_decl_get_sorry_dep]
 def getSorryDep (env : Environment) (declName : Name) : Option Name :=
   match (declMapExt.getState env).find? declName with
-  | some (Decl.fdecl (info := { sorryDep? := dep?, .. }) ..) => dep?
+  | some (.fdecl (info := { sorryDep? := dep?, .. }) ..) => dep?
   | _ => none
 
 end IR
diff --git a/src/Lean/Compiler/IR/ElimDeadBranches.lean b/src/Lean/Compiler/IR/ElimDeadBranches.lean
index cf9e24a4d3..d85163927c 100644
--- a/src/Lean/Compiler/IR/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/IR/ElimDeadBranches.lean
@@ -271,7 +271,7 @@ def inferStep : M Bool := do
   modify fun s => { s with assignments := ctx.decls.map fun _ => {} }
   ctx.decls.size.foldM (init := false) fun idx modified => do
     match ctx.decls[idx]! with
-    | Decl.fdecl (xs := ys) (body := b) .. => do
+    | .fdecl (xs := ys) (body := b) .. => do
       let s ← get
       let currVals := s.funVals[idx]!
       withReader (fun ctx => { ctx with currFnIdx := idx }) do
@@ -280,7 +280,7 @@ def inferStep : M Bool := do
         let s ← get
         let newVals := s.funVals[idx]!
         pure (modified || currVals != newVals)
-    | Decl.extern .. => pure modified
+    | .extern .. => pure modified
 
 partial def inferMain : M Unit := do
   let modified ← inferStep
@@ -305,7 +305,7 @@ partial def elimDeadAux (assignment : Assignment) : FnBody → FnBody
 
 partial def elimDead (assignment : Assignment) (d : Decl) : Decl :=
   match d with
-  | Decl.fdecl (body := b) .. => d.updateBody! <| elimDeadAux assignment b
+  | .fdecl (body := b) .. => d.updateBody! <| elimDeadAux assignment b
   | other => other
 
 end UnreachableBranches
diff --git a/src/Lean/Compiler/IR/ElimDeadVars.lean b/src/Lean/Compiler/IR/ElimDeadVars.lean
index 8cd2cc2447..fe4b421fbe 100644
--- a/src/Lean/Compiler/IR/ElimDeadVars.lean
+++ b/src/Lean/Compiler/IR/ElimDeadVars.lean
@@ -41,7 +41,7 @@ partial def FnBody.elimDead (b : FnBody) : FnBody :=
 /-- Eliminate dead let-declarations and join points -/
 def Decl.elimDead (d : Decl) : Decl :=
   match d with
-  | Decl.fdecl (body := b) .. => d.updateBody! b.elimDead
+  | .fdecl (body := b) .. => d.updateBody! b.elimDead
   | other => other
 
 end Lean.IR
diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean
index 6c71c6ab54..db46c338bd 100644
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -137,7 +137,7 @@ def emitFnDecls : M Unit := do
 def emitMainFn : M Unit := do
   let d ← getDecl `main
   match d with
-  | Decl.fdecl (xs := xs) .. => do
+  | .fdecl (xs := xs) .. => do
     unless xs.size == 2 || xs.size == 1 do throw "invalid main function, incorrect arity when generating code"
     let env ← getEnv
     let usesLeanAPI := usesModuleFrom env `Lean
@@ -644,7 +644,7 @@ def emitDeclAux (d : Decl) : M Unit := do
   withReader (fun ctx => { ctx with jpMap := jpMap }) do
   unless hasInitAttr env d.name do
     match d with
-    | Decl.fdecl (f := f) (xs := xs) (type := t) (body := b) .. =>
+    | .fdecl (f := f) (xs := xs) (type := t) (body := b) .. =>
       let baseName ← toCName f;
       if xs.size == 0 then
         emit "static "
diff --git a/src/Lean/Compiler/IR/EmitUtil.lean b/src/Lean/Compiler/IR/EmitUtil.lean
index bcce85879d..ca6d2caf6a 100644
--- a/src/Lean/Compiler/IR/EmitUtil.lean
+++ b/src/Lean/Compiler/IR/EmitUtil.lean
@@ -26,13 +26,13 @@ abbrev M := ReaderT Environment (StateM NameSet)
   modify fun s => s.insert f
 
 partial def collectFnBody : FnBody → M Unit
-  | FnBody.vdecl _ _ v b   =>
+  | .vdecl _ _ v b   =>
     match v with
-    | Expr.fap f _ => collect f *> collectFnBody b
-    | Expr.pap f _ => collect f *> collectFnBody b
-    | _            => collectFnBody b
-  | FnBody.jdecl _ _ v b   => collectFnBody v *> collectFnBody b
-  | FnBody.case _ _ _ alts => alts.forM fun alt => collectFnBody alt.body
+    | .fap f _ => collect f *> collectFnBody b
+    | .pap f _ => collect f *> collectFnBody b
+    | _        => collectFnBody b
+  | .jdecl _ _ v b   => collectFnBody v *> collectFnBody b
+  | .case _ _ _ alts => alts.forM fun alt => collectFnBody alt.body
   | e => do unless e.isTerminal do collectFnBody e.body
 
 def collectInitDecl (fn : Name) : M Unit := do
@@ -42,8 +42,8 @@ def collectInitDecl (fn : Name) : M Unit := do
   | _           => pure ()
 
 def collectDecl : Decl → M NameSet
-  | Decl.fdecl (f := f) (body := b) .. => collectInitDecl f *> CollectUsedDecls.collectFnBody b *> get
-  | Decl.extern (f := f) .. => collectInitDecl f *> get
+  | .fdecl (f := f) (body := b) .. => collectInitDecl f *> CollectUsedDecls.collectFnBody b *> get
+  | .extern (f := f) .. => collectInitDecl f *> get
 
 end CollectUsedDecls
 
@@ -64,13 +64,13 @@ def collectParams (ps : Array Param) : Collector :=
 
 /-- `collectFnBody` assumes the variables in -/
 partial def collectFnBody : FnBody → Collector
-  | FnBody.vdecl x t _ b    => collectVar x t ∘ collectFnBody b
-  | FnBody.jdecl j xs v b   => collectJP j xs ∘ collectParams xs ∘ collectFnBody v ∘ collectFnBody b
-  | FnBody.case _ _ _ alts  => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s
-  | e                       => if e.isTerminal then id else collectFnBody e.body
+  | .vdecl x t _ b    => collectVar x t ∘ collectFnBody b
+  | .jdecl j xs v b   => collectJP j xs ∘ collectParams xs ∘ collectFnBody v ∘ collectFnBody b
+  | .case _ _ _ alts  => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s
+  | e                 => if e.isTerminal then id else collectFnBody e.body
 
 def collectDecl : Decl → Collector
-  | Decl.fdecl (xs := xs) (body := b) .. => collectParams xs ∘ collectFnBody b
+  | .fdecl (xs := xs) (body := b) .. => collectParams xs ∘ collectFnBody b
   | _ => id
 
 end CollectMaps
diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean
index 9d7363e2f8..e49ca41053 100644
--- a/src/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -14,23 +14,23 @@ namespace CollectProjMap
 abbrev Collector := ProjMap → ProjMap
 @[inline] def collectVDecl (x : VarId) (v : Expr) : Collector := fun m =>
   match v with
-  | Expr.proj ..  => m.insert x v
-  | Expr.sproj .. => m.insert x v
-  | Expr.uproj .. => m.insert x v
-  | _             => m
+  | .proj ..  => m.insert x v
+  | .sproj .. => m.insert x v
+  | .uproj .. => m.insert x v
+  | _         => m
 
 partial def collectFnBody : FnBody → Collector
-  | FnBody.vdecl x _ v b   => collectVDecl x v ∘ collectFnBody b
-  | FnBody.jdecl _ _ v b   => collectFnBody v ∘ collectFnBody b
-  | FnBody.case _ _ _ alts => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s
-  | e                      => if e.isTerminal then id else collectFnBody e.body
+  | .vdecl x _ v b   => collectVDecl x v ∘ collectFnBody b
+  | .jdecl _ _ v b   => collectFnBody v ∘ collectFnBody b
+  | .case _ _ _ alts => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s
+  | e                => if e.isTerminal then id else collectFnBody e.body
 end CollectProjMap
 
 /-- Create a mapping from variables to projections.
    This function assumes variable ids have been normalized -/
 def mkProjMap (d : Decl) : ProjMap :=
   match d with
-  | Decl.fdecl (body := b) .. => CollectProjMap.collectFnBody b {}
+  | .fdecl (body := b) .. => CollectProjMap.collectFnBody b {}
   | _ => {}
 
 structure Context where
@@ -39,12 +39,12 @@ structure Context where
 /-- Return true iff `x` is consumed in all branches of the current block.
    Here consumption means the block contains a `dec x` or `reuse x ...`. -/
 partial def consumed (x : VarId) : FnBody → Bool
-  | FnBody.vdecl _ _ v b   =>
+  | .vdecl _ _ v b   =>
     match v with
     | Expr.reuse y _ _ _ => x == y || consumed x b
     | _                  => consumed x b
-  | FnBody.dec y _ _ _ b   => x == y || consumed x b
-  | FnBody.case _ _ _ alts => alts.all fun alt => consumed x alt.body
+  | .dec y _ _ _ b   => x == y || consumed x b
+  | .case _ _ _ alts => alts.all fun alt => consumed x alt.body
   | e => !e.isTerminal && consumed x e.body
 
 abbrev Mask := Array (Option VarId)
@@ -57,13 +57,13 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
   else
     let b := bs.back
     match b with
-    | (FnBody.vdecl _ _ (Expr.sproj _ _ _) _) => keepInstr b
-    | (FnBody.vdecl _ _ (Expr.uproj _ _) _)   => keepInstr b
-    | (FnBody.inc z n c p _) =>
+    | .vdecl _ _ (.sproj _ _ _) _ => keepInstr b
+    | .vdecl _ _ (.uproj _ _) _   => keepInstr b
+    | .inc z n c p _ =>
       if n == 0 then done () else
       let b' := bs[bs.size - 2]!
       match b' with
-      | (FnBody.vdecl w _ (Expr.proj i x) _) =>
+      | .vdecl w _ (.proj i x) _ =>
         if w == z && y == x then
           /- Found
              ```
@@ -264,7 +264,7 @@ partial def searchAndExpand : FnBody → Array FnBody → M FnBody
 
 def main (d : Decl) : Decl :=
   match d with
-  | Decl.fdecl (body := b) .. =>
+  | .fdecl (body := b) .. =>
     let m := mkProjMap d
     let nextIdx := d.maxIndex + 1
     let bNew := (searchAndExpand b #[] { projMap := m }).run' nextIdx
diff --git a/src/Lean/Compiler/IR/FreeVars.lean b/src/Lean/Compiler/IR/FreeVars.lean
index 848fce0309..8a1aae2c64 100644
--- a/src/Lean/Compiler/IR/FreeVars.lean
+++ b/src/Lean/Compiler/IR/FreeVars.lean
@@ -73,8 +73,8 @@ partial def collectFnBody : FnBody → Collector
   | FnBody.unreachable      => skip
 
 partial def collectDecl : Decl → Collector
-  | Decl.fdecl (xs := xs) (body := b) .. => collectParams xs >> collectFnBody b
-  | Decl.extern (xs := xs) ..            => collectParams xs
+  | .fdecl (xs := xs) (body := b) .. => collectParams xs >> collectFnBody b
+  | .extern (xs := xs) ..            => collectParams xs
 
 end MaxIndex
 
diff --git a/src/Lean/Compiler/IR/NormIds.lean b/src/Lean/Compiler/IR/NormIds.lean
index 02ee71405d..e9eafe8f3b 100644
--- a/src/Lean/Compiler/IR/NormIds.lean
+++ b/src/Lean/Compiler/IR/NormIds.lean
@@ -18,14 +18,14 @@ def checkParams (ps : Array Param) : M Bool :=
   ps.allM fun p => checkId p.x.idx
 
 partial def checkFnBody : FnBody → M Bool
-  | FnBody.vdecl x _ _ b    => checkId x.idx <&&> checkFnBody b
-  | FnBody.jdecl j ys _ b   => checkId j.idx <&&> checkParams ys <&&> checkFnBody b
-  | FnBody.case _ _ _ alts  => alts.allM fun alt => checkFnBody alt.body
-  | b                       => if b.isTerminal then pure true else checkFnBody b.body
+  | .vdecl x _ _ b    => checkId x.idx <&&> checkFnBody b
+  | .jdecl j ys _ b   => checkId j.idx <&&> checkParams ys <&&> checkFnBody b
+  | .case _ _ _ alts  => alts.allM fun alt => checkFnBody alt.body
+  | b                 => if b.isTerminal then pure true else checkFnBody b.body
 
 partial def checkDecl : Decl → M Bool
-  | Decl.fdecl (xs := xs) (body := b) .. => checkParams xs <&&> checkFnBody b
-  | Decl.extern (xs := xs) .. => checkParams xs
+  | .fdecl (xs := xs) (body := b) .. => checkParams xs <&&> checkFnBody b
+  | .extern (xs := xs) .. => checkParams xs
 
 end UniqueIds
 
diff --git a/src/Lean/Compiler/IR/PushProj.lean b/src/Lean/Compiler/IR/PushProj.lean
index 4a30505ced..178d8f24c3 100644
--- a/src/Lean/Compiler/IR/PushProj.lean
+++ b/src/Lean/Compiler/IR/PushProj.lean
@@ -40,7 +40,7 @@ partial def FnBody.pushProj (b : FnBody) : FnBody :=
   let (bs, term) := b.flatten
   let bs         := modifyJPs bs pushProj
   match term with
-  | FnBody.case tid x xType alts =>
+  | .case tid x xType alts =>
     let altsF      := alts.map fun alt => alt.body.freeIndices
     let (bs, alts) := pushProjs bs alts altsF #[] (mkIndexSet x.idx)
     let alts       := alts.map fun alt => alt.modifyBody pushProj
@@ -51,7 +51,7 @@ partial def FnBody.pushProj (b : FnBody) : FnBody :=
 /-- Push projections inside `case` branches. -/
 def Decl.pushProj (d : Decl) : Decl :=
   match d with
-  | Decl.fdecl (body := b) .. => d.updateBody! b.pushProj |>.normalizeIds
+  | .fdecl (body := b) .. => d.updateBody! b.pushProj |>.normalizeIds
   | other => other
 
 end Lean.IR
diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean
index c45b640251..4071b008cd 100644
--- a/src/Lean/Compiler/IR/RC.lean
+++ b/src/Lean/Compiler/IR/RC.lean
@@ -266,7 +266,7 @@ partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet)
 
 partial def visitDecl (env : Environment) (decls : Array Decl) (d : Decl) : Decl :=
   match d with
-  | Decl.fdecl (xs := xs) (body := b) .. =>
+  | .fdecl (xs := xs) (body := b) .. =>
     let ctx : Context  := { env := env, decls := decls }
     let ctx := updateVarInfoWithParams ctx xs
     let (b, bLiveVars) := visitFnBody b ctx
diff --git a/src/Lean/Compiler/IR/ResetReuse.lean b/src/Lean/Compiler/IR/ResetReuse.lean
index 2793c7e402..9566eb5758 100644
--- a/src/Lean/Compiler/IR/ResetReuse.lean
+++ b/src/Lean/Compiler/IR/ResetReuse.lean
@@ -150,7 +150,7 @@ open ResetReuse
 
 def Decl.insertResetReuse (d : Decl) : Decl :=
   match d with
-  | Decl.fdecl (body := b) ..=>
+  | .fdecl (body := b) ..=>
     let nextIndex := d.maxIndex + 1
     let bNew      := (R b {}).run' nextIndex
     d.updateBody! bNew
diff --git a/src/Lean/Compiler/IR/SimpCase.lean b/src/Lean/Compiler/IR/SimpCase.lean
index 11053f2dde..17b13f41ce 100644
--- a/src/Lean/Compiler/IR/SimpCase.lean
+++ b/src/Lean/Compiler/IR/SimpCase.lean
@@ -71,7 +71,7 @@ partial def FnBody.simpCase (b : FnBody) : FnBody :=
   - Merge most common branches using `Alt.default`. -/
 def Decl.simpCase (d : Decl) : Decl :=
   match d with
-  | Decl.fdecl (body := b) .. => d.updateBody! b.simpCase
+  | .fdecl (body := b) .. => d.updateBody! b.simpCase
   | other => other
 
 end Lean.IR
diff --git a/src/Lean/Compiler/IR/Sorry.lean b/src/Lean/Compiler/IR/Sorry.lean
index 4d1e05f6a1..8417dc145b 100644
--- a/src/Lean/Compiler/IR/Sorry.lean
+++ b/src/Lean/Compiler/IR/Sorry.lean
@@ -30,14 +30,14 @@ where
     else if let some g := (← get).localSorryMap.find? f then
       found g
     else match (← findDecl f) with
-      | Decl.fdecl (info := { sorryDep? := some g, .. }) .. => found g
+      | some (.fdecl (info := { sorryDep? := some g, .. }) ..) => found g
       | _ => return ()
 
 partial def visitFndBody (b : FnBody) : ExceptT Name M Unit := do
   match b with
-  | FnBody.vdecl _ _ v b   => visitExpr v; visitFndBody b
-  | FnBody.jdecl _ _ v b   => visitFndBody v; visitFndBody b
-  | FnBody.case _ _ _ alts => alts.forM fun alt => visitFndBody alt.body
+  | .vdecl _ _ v b   => visitExpr v; visitFndBody b
+  | .jdecl _ _ v b   => visitFndBody v; visitFndBody b
+  | .case _ _ _ alts => alts.forM fun alt => visitFndBody alt.body
   | _ =>
     unless b.isTerminal do
       let (_, b) := b.split
@@ -45,13 +45,13 @@ partial def visitFndBody (b : FnBody) : ExceptT Name M Unit := do
 
 def visitDecl (d : Decl) : M Unit := do
   match d with
-  | Decl.fdecl (f := f) (body := b) .. =>
+  | .fdecl (f := f) (body := b) .. =>
     match (← get).localSorryMap.find? f with
     | some _ => return ()
     | none =>
       match (← visitFndBody b |>.run) with
-      | Except.ok _    => return ()
-      | Except.error g =>
+      | .ok _    => return ()
+      | .error g =>
         modify fun s => {
           localSorryMap := s.localSorryMap.insert f g
           modified      := true
diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean
index 7483c659db..7789a74fb8 100644
--- a/src/Lean/Elab/InfoTree/Main.lean
+++ b/src/Lean/Elab/InfoTree/Main.lean
@@ -115,8 +115,8 @@ def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
 
 def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
   match info with
-  | CompletionInfo.dot i (expectedType? := expectedType?) .. => return f!"[.] {← i.format ctx} : {expectedType?}"
-  | CompletionInfo.id stx _ _ lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
+  | .dot i (expectedType? := expectedType?) .. => return f!"[.] {← i.format ctx} : {expectedType?}"
+  | .id stx _ _ lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
   | _ => return f!"[.] {info.stx} @ {formatStxRange ctx info.stx}"
 
 def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 0680a78ad0..a9d398e536 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -678,7 +678,7 @@ partial def visit (e : Expr) : M Unit := do
     | .fvar fvarId ..    =>
       match (← fvarId.getDecl) with
       | .cdecl .. => return ()
-      | LocalDecl.ldecl (value := v) .. => visit v
+      | .ldecl (value := v) .. => visit v
     | .mvar mvarId ..    =>
       let e' ← instantiateMVars e
       if e' != e then
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 548ed43445..ce67aaadf7 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -1420,10 +1420,10 @@ end Methods
 
 def isInductivePredicate (declName : Name) : MetaM Bool := do
   match (← getEnv).find? declName with
-  | some (ConstantInfo.inductInfo { type := type, ..}) =>
+  | some (.inductInfo { type := type, ..}) =>
     forallTelescopeReducing type fun _ type => do
       match (← whnfD type) with
-      | Expr.sort u .. => return u == levelZero
+      | .sort u .. => return u == levelZero
       | _ => return false
   | _ => return false
 
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index e656668911..df2f925819 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -163,10 +163,10 @@ where
       xs.forM fun x => do
         let xDecl ← getFVarLocalDecl x;
         match xDecl with
-        | LocalDecl.cdecl (type := t) .. =>
+        | .cdecl (type := t) .. =>
           ensureType t
           check t
-        | LocalDecl.ldecl (type := t) (value := v) .. =>
+        | .ldecl (type := t) (value := v) .. =>
           ensureType t
           check t
           let vType ← inferType v
diff --git a/src/Lean/Meta/CollectFVars.lean b/src/Lean/Meta/CollectFVars.lean
index d4bafed016..f787070eea 100644
--- a/src/Lean/Meta/CollectFVars.lean
+++ b/src/Lean/Meta/CollectFVars.lean
@@ -16,8 +16,8 @@ def Expr.collectFVars (e : Expr) : StateRefT CollectFVars.State MetaM Unit := do
 
 def LocalDecl.collectFVars (localDecl : LocalDecl) : StateRefT CollectFVars.State MetaM Unit := do
   match localDecl with
-  | LocalDecl.cdecl (type := type) .. => type.collectFVars
-  | LocalDecl.ldecl (type := type) (value := value) .. => type.collectFVars; value.collectFVars
+  | .cdecl (type := type) .. => type.collectFVars
+  | .ldecl (type := type) (value := value) .. => type.collectFVars; value.collectFVars
 
 /-- For each variable in `s.fvarSet`, include its dependencies. -/
 partial def CollectFVars.State.addDependencies (s : CollectFVars.State) : MetaM CollectFVars.State := do
diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index 2d12df47e1..0bb11590eb 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -541,7 +541,7 @@ partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
   withReducible do
     let (k, args) ← getUnifyKeyArgs e (root := true)
     match k with
-    | Key.star => d.root.foldlM (init := #[]) fun result k c => process k.arity #[] c result
+    | .star => d.root.foldlM (init := #[]) fun result k c => process k.arity #[] c result
     | _ =>
       let result := getStarResult d
       match d.root.find? k with
@@ -575,9 +575,9 @@ where
           | none   => return result
           | some c => process 0 (todo ++ args) c.2 result
         match k with
-        | Key.star  => cs.foldlM (init := result) fun result ⟨k, c⟩ => process k.arity todo c result
+        | .star  => cs.foldlM (init := result) fun result ⟨k, c⟩ => process k.arity todo c result
         -- See comment a `getMatch` regarding non-dependent arrows vs dependent arrows
-        | Key.arrow => visitNonStar Key.other #[] (← visitNonStar k args (← visitStar result))
-        | _         => visitNonStar k args (← visitStar result)
+        | .arrow => visitNonStar Key.other #[] (← visitNonStar k args (← visitStar result))
+        | _      => visitNonStar k args (← visitStar result)
 
 end Lean.Meta.DiscrTree
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index d4bd948f59..546dec1ad8 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -673,7 +673,7 @@ mutual
     else
       let lctx := ctxMeta.lctx
       match lctx.findFVar? fvar with
-      | some (LocalDecl.ldecl (value := v) ..) => visit check v
+      | some (.ldecl (value := v) ..) => visit check v
       | _ =>
         if ctx.fvars.contains fvar then pure fvar
         else
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 28c3858739..a870ffc40e 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -283,21 +283,21 @@ end
 /-- Auxiliary combinator for handling easy WHNF cases. It takes a function for handling the "hard" cases as an argument -/
 @[specialize] partial def whnfEasyCases (e : Expr) (k : Expr → MetaM Expr) : MetaM Expr := do
   match e with
-  | Expr.forallE ..    => return e
-  | Expr.lam ..        => return e
-  | Expr.sort ..       => return e
-  | Expr.lit ..        => return e
-  | Expr.bvar ..       => unreachable!
-  | Expr.letE ..       => k e
-  | Expr.const ..      => k e
-  | Expr.app ..        => k e
-  | Expr.proj ..       => k e
-  | Expr.mdata _ e     => whnfEasyCases e k
-  | Expr.fvar fvarId   =>
+  | .forallE ..    => return e
+  | .lam ..        => return e
+  | .sort ..       => return e
+  | .lit ..        => return e
+  | .bvar ..       => unreachable!
+  | .letE ..       => k e
+  | .const ..      => k e
+  | .app ..        => k e
+  | .proj ..       => k e
+  | .mdata _ e     => whnfEasyCases e k
+  | .fvar fvarId   =>
     let decl ← fvarId.getDecl
     match decl with
-    | LocalDecl.cdecl .. => return e
-    | LocalDecl.ldecl (value := v) (nonDep := nonDep) .. =>
+    | .cdecl .. => return e
+    | .ldecl (value := v) (nonDep := nonDep) .. =>
       let cfg ← getConfig
       if nonDep && !cfg.zetaNonDep then
         return e
@@ -305,7 +305,7 @@ end
         if cfg.trackZeta then
           modify fun s => { s with zetaFVarIds := s.zetaFVarIds.insert fvarId }
         whnfEasyCases v k
-  | Expr.mvar mvarId   =>
+  | .mvar mvarId   =>
     match (← getExprMVarAssignment? mvarId) with
     | some v => whnfEasyCases v k
     | none   => return e
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index d0688ef4c3..e26a4e2ab0 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -676,8 +676,8 @@ end DependsOn
   depends on a free variable `x` s.t. `pf x` is `true` or an unassigned metavariable `?m` s.t. `pm ?m` is true. -/
 @[inline] def findLocalDeclDependsOn [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (pf : FVarId → Bool := fun _ => false) (pm : MVarId → Bool := fun _ => false) : m Bool := do
   match localDecl with
-  | LocalDecl.cdecl (type := t) ..  => findExprDependsOn t pf pm
-  | LocalDecl.ldecl (type := t) (value := v) .. =>
+  | .cdecl (type := t) ..  => findExprDependsOn t pf pm
+  | .ldecl (type := t) (value := v) .. =>
     let (result, { mctx, .. }) := (DependsOn.main pf pm t <||> DependsOn.main pf pm v).run { mctx := (← getMCtx) }
     setMCtx mctx
     return result
diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index 9886debc1b..890781a3b0 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -421,10 +421,10 @@ partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTr
   match infoTree.foldInfo (init := none) (choose fileMap hoverLine) with
   | some (hoverInfo, ctx, Info.ofCompletionInfo info) =>
     match info with
-    | CompletionInfo.dot info (expectedType? := expectedType?) .. => dotCompletion ctx info hoverInfo expectedType?
-    | CompletionInfo.id _   id danglingDot lctx expectedType? => idCompletion ctx lctx id hoverInfo danglingDot expectedType?
-    | CompletionInfo.option stx => optionCompletion ctx stx caps
-    | CompletionInfo.tactic .. => tacticCompletion ctx
+    | .dot info (expectedType? := expectedType?) .. => dotCompletion ctx info hoverInfo expectedType?
+    | .id _   id danglingDot lctx expectedType? => idCompletion ctx lctx id hoverInfo danglingDot expectedType?
+    | .option stx => optionCompletion ctx stx caps
+    | .tactic .. => tacticCompletion ctx
     | _ => return none
   | _ =>
     -- TODO try to extract id from `fileMap` and some `ContextInfo` from `InfoTree`
diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean
index 1a5adf2720..58e3410b5c 100644
--- a/src/Lean/Structure.lean
+++ b/src/Lean/Structure.lean
@@ -68,7 +68,7 @@ def getStructureInfo? (env : Environment) (structName : Name) : Option Structure
 
 def getStructureCtor (env : Environment) (constName : Name) : ConstructorVal :=
   match env.find? constName with
-  | some (ConstantInfo.inductInfo { isRec := false, ctors := [ctorName], .. }) =>
+  | some (.inductInfo { isRec := false, ctors := [ctorName], .. }) =>
     match env.find? ctorName with
     | some (ConstantInfo.ctorInfo val) => val
     | _ => panic! "ill-formed environment"
@@ -193,15 +193,15 @@ def getPathToBaseStructure? (env : Environment) (baseStructName : Name) (structN
 /-- Return true iff `constName` is the a non-recursive inductive datatype that has only one constructor. -/
 def isStructureLike (env : Environment) (constName : Name) : Bool :=
   match env.find? constName with
-  | some (ConstantInfo.inductInfo { isRec := false, ctors := [_], numIndices := 0, .. }) => true
+  | some (.inductInfo { isRec := false, ctors := [_], numIndices := 0, .. }) => true
   | _ => false
 
 /-- Return number of fields for a structure-like type -/
 def getStructureLikeNumFields (env : Environment) (constName : Name) : Nat :=
   match env.find? constName with
-  | some (ConstantInfo.inductInfo { isRec := false, ctors := [ctor], numIndices := 0, .. }) =>
+  | some (.inductInfo { isRec := false, ctors := [ctor], numIndices := 0, .. }) =>
     match env.find? ctor with
-    | some (ConstantInfo.ctorInfo { numFields := n, .. }) => n
+    | some (.ctorInfo { numFields := n, .. }) => n
     | _ => 0
   | _ => 0
 
diff --git a/src/Lean/Util/FindLevelMVar.lean b/src/Lean/Util/FindLevelMVar.lean
index 4270adfcf9..f6ce8d0404 100644
--- a/src/Lean/Util/FindLevelMVar.lean
+++ b/src/Lean/Util/FindLevelMVar.lean
@@ -16,26 +16,26 @@ mutual
     if s.isSome || !e.hasLevelMVar then s else main p e s
 
   partial def main (p : LMVarId → Bool) : Expr → Visitor
-    | Expr.sort l          => visitLevel p l
-    | Expr.const _ ls      => ls.foldr (init := id) fun l acc => visitLevel p l ∘ acc
-    | Expr.forallE _ d b _ => visit p b ∘ visit p d
-    | Expr.lam _ d b _     => visit p b ∘ visit p d
-    | Expr.letE _ t v b _  => visit p b ∘ visit p v ∘ visit p t
-    | Expr.app f a         => visit p a ∘ visit p f
-    | Expr.mdata _ b       => visit p b
-    | Expr.proj _ _ e      => visit p e
+    | .sort l          => visitLevel p l
+    | .const _ ls      => ls.foldr (init := id) fun l acc => visitLevel p l ∘ acc
+    | .forallE _ d b _ => visit p b ∘ visit p d
+    | .lam _ d b _     => visit p b ∘ visit p d
+    | .letE _ t v b _  => visit p b ∘ visit p v ∘ visit p t
+    | .app f a         => visit p a ∘ visit p f
+    | .mdata _ b       => visit p b
+    | .proj _ _ e      => visit p e
     | _                    => id
 
   partial def visitLevel (p : LMVarId → Bool) (l : Level) : Visitor := fun s =>
     if s.isSome || !l.hasMVar then s else mainLevel p l s
 
   partial def mainLevel (p : LMVarId → Bool) : Level → Visitor
-    | Level.zero        => id
-    | Level.succ l      => visitLevel p l
-    | Level.max l₁ l₂   => visitLevel p l₁ ∘ visitLevel p l₂
-    | Level.imax l₁ l₂  => visitLevel p l₁ ∘ visitLevel p l₂
-    | Level.param _     => id
-    | Level.mvar mvarId => fun s => if p mvarId then some mvarId else s
+    | .zero        => id
+    | .succ l      => visitLevel p l
+    | .max l₁ l₂   => visitLevel p l₁ ∘ visitLevel p l₂
+    | .imax l₁ l₂  => visitLevel p l₁ ∘ visitLevel p l₂
+    | .param _     => id
+    | .mvar mvarId => fun s => if p mvarId then some mvarId else s
 end
 
 end FindLevelMVar