diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean
index 35f8075690..4b0d64c840 100644
--- a/src/Lean/Compiler/IR/Basic.lean
+++ b/src/Lean/Compiler/IR/Basic.lean
@@ -45,7 +45,7 @@ abbrev MData.empty : MData := {}
       because it is 32-bit in 32-bit machines, and 64-bit in 64-bit machines,
       and we want the C++ backend for our Compiler to generate platform independent code.
 
-   - `irrelevant` for Lean types, propositions and proofs.
+   - `erased` for Lean types, propositions and proofs.
 
    - `object` a pointer to a value in the heap.
 
@@ -73,7 +73,7 @@ then one of the following must hold in each (execution) branch.
 -/
 inductive IRType where
   | float | uint8 | uint16 | uint32 | uint64 | usize
-  | irrelevant | object | tobject
+  | erased | object | tobject
   | float32
   | struct (leanTypeName : Option Name) (types : Array IRType) : IRType
   | union (leanTypeName : Name) (types : Array IRType) : IRType
@@ -96,24 +96,24 @@ def isObj : IRType → Bool
   | tobject => true
   | _       => false
 
-def isIrrelevant : IRType → Bool
-  | irrelevant => true
+def isErased : IRType → Bool
+  | erased => true
   | _ => false
 
 end IRType
 
 /-- Arguments to applications, constructors, etc.
-   We use `irrelevant` for Lean types, propositions and proofs that have been erased.
+   We use `erased` for Lean types, propositions and proofs that have been erased.
    Recall that for a Function `f`, we also generate `f._rarg` which does not take
-   `irrelevant` arguments. However, `f._rarg` is only safe to be used in full applications. -/
+   `erased` arguments. However, `f._rarg` is only safe to be used in full applications. -/
 inductive Arg where
   | var (id : VarId)
-  | irrelevant
+  | erased
   deriving Inhabited, BEq, Repr
 
 protected def Arg.beq : Arg → Arg → Bool
   | var x,      var y      => x == y
-  | irrelevant, irrelevant => true
+  | erased, erased         => true
   | _,          _          => false
 
 inductive LitVal where
@@ -201,7 +201,7 @@ inductive FnBody where
   /-- Store `y : Usize` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. -/
   | uset (x : VarId) (i : Nat) (y : VarId) (b : FnBody)
   /-- Store `y : ty` at Position `sizeof(void*)*i + offset` in `x`. `x` must be a Constructor object and `RC(x)` must be 1.
-  `ty` must not be `object`, `tobject`, `irrelevant` nor `Usize`. -/
+  `ty` must not be `object`, `tobject`, `erased` nor `Usize`. -/
   | sset (x : VarId) (i : Nat) (offset : Nat) (y : VarId) (ty : IRType) (b : FnBody)
   /-- RC increment for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not.
   If `persistent == true` then `x` is statically known to be a persistent object. -/
@@ -445,7 +445,7 @@ instance : AlphaEqv VarId := ⟨VarId.alphaEqv⟩
 
 def Arg.alphaEqv (ρ : IndexRenaming) : Arg → Arg → Bool
   | Arg.var v₁,     Arg.var v₂     => aeqv ρ v₁ v₂
-  | Arg.irrelevant, Arg.irrelevant => true
+  | Arg.erased,     Arg.erased     => true
   | _,              _              => false
 
 instance : AlphaEqv Arg := ⟨Arg.alphaEqv⟩
diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean
index 7d39093307..7e3c78224c 100644
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/src/Lean/Compiler/IR/Boxing.lean
@@ -92,7 +92,7 @@ def eqvTypes (t₁ t₂ : IRType) : Bool :=
 structure BoxingContext where
   f : FunId := default
   localCtx : LocalContext := {}
-  resultType : IRType := IRType.irrelevant
+  resultType : IRType := .erased
   decls : Array Decl
   env : Environment
 
@@ -222,7 +222,7 @@ def castArgsIfNeededAux (xs : Array Arg) (typeFromIdx : Nat → IRType) : M (Arr
   for x in xs do
     let expected := typeFromIdx i
     match x with
-    | Arg.irrelevant =>
+    | Arg.erased =>
       xs' := xs'.push x
     | Arg.var x =>
       let xType ← getVarType x
diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean
index b45ea2eaee..2cf7d62170 100644
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -63,7 +63,7 @@ def toCType : IRType → String
   | IRType.usize      => "size_t"
   | IRType.object     => "lean_object*"
   | IRType.tobject    => "lean_object*"
-  | IRType.irrelevant => "lean_object*"
+  | IRType.erased     => "lean_object*"
   | IRType.struct _ _ => panic! "not implemented yet"
   | IRType.union _ _  => panic! "not implemented yet"
 
@@ -104,8 +104,8 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M U
   emit (toCType decl.resultType ++ " " ++ cppBaseName)
   unless ps.isEmpty do
     emit "("
-    -- We omit irrelevant parameters for extern constants
-    let ps := if isExternC env decl.name then ps.filter (fun p => !p.ty.isIrrelevant) else ps
+    -- We omit erased parameters for extern constants
+    let ps := if isExternC env decl.name then ps.filter (fun p => !p.ty.isErased) else ps
     if ps.size > closureMaxArgs && isBoxedName decl.name then
       emit "lean_object**"
     else
@@ -405,10 +405,10 @@ def toStringArgs (ys : Array Arg) : List String :=
 
 def emitSimpleExternalCall (f : String) (ps : Array Param) (ys : Array Arg) : M Unit := do
   emit f; emit "("
-  -- We must remove irrelevant arguments to extern calls.
+  -- We must remove erased arguments to extern calls.
   discard <| ys.size.foldM
     (fun i _ (first : Bool) =>
-      if ps[i]!.ty.isIrrelevant then
+      if ps[i]!.ty.isErased then
         pure first
       else do
         unless first do emit ", "
diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean
index f38b71a630..b2f99e3f54 100644
--- a/src/Lean/Compiler/IR/EmitLLVM.lean
+++ b/src/Lean/Compiler/IR/EmitLLVM.lean
@@ -323,7 +323,7 @@ def toLLVMType (t : IRType) : M llvmctx (LLVM.LLVMType llvmctx) := do
   | IRType.usize      => LLVM.size_tType llvmctx
   | IRType.object     => do LLVM.pointerType (← LLVM.i8Type llvmctx)
   | IRType.tobject    => do LLVM.pointerType (← LLVM.i8Type llvmctx)
-  | IRType.irrelevant => do LLVM.pointerType (← LLVM.i8Type llvmctx)
+  | IRType.erased     => do LLVM.pointerType (← LLVM.i8Type llvmctx)
   | IRType.struct _ _ => panic! "not implemented yet"
   | IRType.union _ _  => panic! "not implemented yet"
 
@@ -485,8 +485,8 @@ def emitFnDeclAux (mod : LLVM.Module llvmctx)
         let retty ← (toLLVMType decl.resultType)
         let mut argtys := #[]
         for p in ps do
-          -- if it is extern, then we must not add irrelevant args
-          if !(isExternC env decl.name) || !p.ty.isIrrelevant then
+          -- if it is extern, then we must not add erased args
+          if !(isExternC env decl.name) || !p.ty.isErased then
             argtys := argtys.push (← toLLVMType p.ty)
         -- TODO (bollu): simplify this API, this code of `closureMaxArgs` is duplicated in multiple places.
         if argtys.size > closureMaxArgs && isBoxedName decl.name then
@@ -551,8 +551,8 @@ def emitArgSlot_ (builder : LLVM.Builder llvmctx)
   | Arg.var x => emitLhsSlot_ x
   | _ => do
     let slotty ← LLVM.voidPtrType llvmctx
-    let slot ← buildPrologueAlloca builder slotty "irrelevant_slot"
-    let v ← callLeanBox builder (← constIntSizeT 0) "irrelevant_val"
+    let slot ← buildPrologueAlloca builder slotty "erased_slot"
+    let v ← callLeanBox builder (← constIntSizeT 0) "erased_val"
     let _ ← LLVM.buildStore builder v slot
     return (slotty, slot)
 
@@ -645,7 +645,7 @@ def emitSimpleExternalCall (builder : LLVM.Builder llvmctx)
   let mut args := #[]
   let mut argTys := #[]
   for (p, y) in ps.zip ys do
-    if !p.ty.isIrrelevant then
+    if !p.ty.isErased then
       let (_yty, yv) ← emitArgVal builder y ""
       argTys := argTys.push (← toLLVMType p.ty)
       args := args.push yv
diff --git a/src/Lean/Compiler/IR/Format.lean b/src/Lean/Compiler/IR/Format.lean
index 6334c121f9..197bd546d2 100644
--- a/src/Lean/Compiler/IR/Format.lean
+++ b/src/Lean/Compiler/IR/Format.lean
@@ -10,8 +10,8 @@ namespace Lean
 namespace IR
 
 private def formatArg : Arg → Format
-  | Arg.var id     => format id
-  | Arg.irrelevant => "◾"
+  | Arg.var id => format id
+  | Arg.erased => "◾"
 
 instance : ToFormat Arg := ⟨formatArg⟩
 
@@ -61,7 +61,7 @@ private partial def formatIRType : IRType → Format
   | IRType.uint32       => "u32"
   | IRType.uint64       => "u64"
   | IRType.usize        => "usize"
-  | IRType.irrelevant   => "◾"
+  | IRType.erased       => "◾"
   | IRType.object       => "obj"
   | IRType.tobject      => "tobj"
   | IRType.struct _ tys =>
diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean
index 2979099f18..6b02991660 100644
--- a/src/Lean/Compiler/IR/RC.lean
+++ b/src/Lean/Compiler/IR/RC.lean
@@ -87,8 +87,8 @@ private def isBorrowParamAux (x : VarId) (ys : Array Arg) (consumeParamPred : Na
   ys.size.any fun i _ =>
     let y := ys[i]
     match y with
-    | Arg.irrelevant => false
-    | Arg.var y      => x == y && !consumeParamPred i
+    | Arg.erased => false
+    | Arg.var y  => x == y && !consumeParamPred i
 
 private def isBorrowParam (x : VarId) (ys : Array Arg) (ps : Array Param) : Bool :=
   isBorrowParamAux x ys fun i => ! ps[i]!.borrow
@@ -102,14 +102,14 @@ private def getNumConsumptions (x : VarId) (ys : Array Arg) (consumeParamPred :
   ys.size.fold (init := 0) fun i _ n =>
     let y := ys[i]
     match y with
-    | Arg.irrelevant => n
-    | Arg.var y      => if x == y && consumeParamPred i then n+1 else n
+    | Arg.erased => n
+    | Arg.var y  => if x == y && consumeParamPred i then n+1 else n
 
 private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred : Nat → Bool) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody :=
   xs.size.fold (init := b) fun i _ b =>
     let x := xs[i]
     match x with
-    | Arg.irrelevant => b
+    | Arg.erased => b
     | Arg.var x =>
       let info := getVarInfo ctx x
       if !info.ref || !isFirstOcc xs i then b
@@ -130,8 +130,8 @@ private def addIncBefore (ctx : Context) (xs : Array Arg) (ps : Array Param) (b
 private def addDecAfterFullApp (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody :=
 xs.size.fold (init := b) fun i _ b =>
   match xs[i] with
-  | Arg.irrelevant => b
-  | Arg.var x      =>
+  | Arg.erased => b
+  | Arg.var x  =>
     /- We must add a `dec` if `x` must be consumed, it is alive after the application,
        and it has been borrowed by the application.
        Remark: `x` may occur multiple times in the application (e.g., `f x y x`).
diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean
index 3cf2ff6477..d4949a8291 100644
--- a/src/Lean/Compiler/IR/ToIR.lean
+++ b/src/Lean/Compiler/IR/ToIR.lean
@@ -77,9 +77,9 @@ def lowerArg (a : LCNF.Arg) : M Arg := do
   | .fvar fvarId =>
     match (← get).fvars[fvarId]? with
     | some (.var varId) => return .var varId
-    | some .erased => return .irrelevant
+    | some .erased => return .erased
     | some (.joinPoint ..) | none => panic! "unexpected value"
-  | .erased | .type .. => return .irrelevant
+  | .erased | .type .. => return .erased
 
 inductive TranslatedProj where
   | expr (e : Expr)
@@ -92,7 +92,7 @@ def lowerProj (base : VarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo)
   | .object i => ⟨.expr (.proj i base), .object⟩
   | .usize i => ⟨.expr (.uproj i base), .usize⟩
   | .scalar _ offset irType => ⟨.expr (.sproj (ctorInfo.size + ctorInfo.usize) offset base), irType⟩
-  | .irrelevant => ⟨.erased, .irrelevant⟩
+  | .erased => ⟨.erased, .erased⟩
 
 def lowerParam (p : LCNF.Param) : M Param := do
   let x ← bindVar p.fvarId
@@ -124,7 +124,7 @@ partial def lowerCode (c : LCNF.Code) : M FnBody := do
   | .return fvarId =>
     let arg := match (← get).fvars[fvarId]? with
     | some (.var varId) => .var varId
-    | some .erased => .irrelevant
+    | some .erased => .erased
     | some (.joinPoint ..) | none => panic! "unexpected value"
     return .ret arg
   | .unreach .. => return .unreachable
@@ -176,7 +176,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
           match fields[i] with
           | .object .. =>
             result := result.push irArgs[i]!
-          | .usize .. | .scalar .. | .irrelevant => pure ()
+          | .usize .. | .scalar .. | .erased => pure ()
         pure result
       let objVar ← bindVar decl.fvarId
       let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
@@ -190,8 +190,8 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
             | .scalar _ offset argType =>
               let k ← loop (i + 1)
               return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
-            | .object .. | .irrelevant => loop (i + 1)
-          | some .irrelevant => loop (i + 1)
+            | .object .. | .erased => loop (i + 1)
+          | some .erased => loop (i + 1)
           | none => lowerCode k
         loop 0
       return .vdecl objVar type (.ctor ctorInfo objArgs) (← lowerNonObjectFields ())
diff --git a/src/Lean/Compiler/IR/ToIRType.lean b/src/Lean/Compiler/IR/ToIRType.lean
index b54094f2f1..7e91bf8e83 100644
--- a/src/Lean/Compiler/IR/ToIRType.lean
+++ b/src/Lean/Compiler/IR/ToIRType.lean
@@ -46,7 +46,7 @@ where fillCache : CoreM IRType := do
     | ``USize => return .usize
     | ``Float => return .float
     | ``Float32 => return .float32
-    | ``lcErased => return .irrelevant
+    | ``lcErased => return .erased
     | _ =>
       let env ← Lean.getEnv
       let some (.inductInfo inductiveVal) := env.find? name | return .object
@@ -77,7 +77,7 @@ def toIRType (type : Lean.Expr) : CoreM IRType := do
   | _ => unreachable!
 
 inductive CtorFieldInfo where
-  | irrelevant
+  | erased
   | object (i : Nat)
   | usize  (i : Nat)
   | scalar (sz : Nat) (offset : Nat) (type : IRType)
@@ -86,7 +86,7 @@ inductive CtorFieldInfo where
 namespace CtorFieldInfo
 
 def format : CtorFieldInfo → Format
-  | irrelevant => "◾"
+  | erased => "◾"
   | object i   => f!"obj@{i}"
   | usize i    => f!"usize@{i}"
   | scalar sz offset type => f!"scalar#{sz}@{offset}:{type}"
@@ -129,7 +129,7 @@ where fillCache := do
         nextIdx := nextIdx + 1
         pure <| .object i
       | .usize => pure <| .usize 0
-      | .irrelevant => .pure <| .irrelevant
+      | .erased => .pure <| .erased
       | .uint8 =>
         has1BScalar := true
         .pure <| .scalar 1 0 .uint8
@@ -156,7 +156,7 @@ where fillCache := do
       | .usize _ => do
         let i ← modifyGet fun nextIdx => (nextIdx, nextIdx + 1)
         return .usize i
-      | .object _ | .scalar .. | .irrelevant => return field
+      | .object _ | .scalar .. | .erased => return field
     let numUSize := nextIdx - numObjs
     let adjustScalarsForSize (fields : Array CtorFieldInfo) (size : Nat) (nextOffset : Nat)
         : Array CtorFieldInfo × Nat :=
@@ -168,7 +168,7 @@ where fillCache := do
             return .scalar sz offset type
           else
             return field
-        | .object _ | .usize _ | .irrelevant => return field
+        | .object _ | .usize _ | .erased => return field
     let mut nextOffset := 0
     if has8BScalar then
       ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 8 nextOffset