chore: deprecate levelZero and levelOne

src/Lean/Elab/BuiltinNotation.lean

@@ -542,8 +542,8 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
   let mut mStx := stx[2]
   if mStx.getKind == ``Lean.Parser.Term.macroDollarArg then
     mStx := mStx[1]
-  let m ← elabTerm mStx (← mkArrow (mkSort levelOne) (mkSort levelOne))
-  let ω ← mkFreshExprMVar (mkSort levelOne)
+  let m ← elabTerm mStx (← mkArrow (mkSort Level.one) (mkSort Level.one))
+  let ω ← mkFreshExprMVar (mkSort Level.one)
   let stWorld ← mkAppM ``STWorld #[ω, m]
   discard <| mkInstMVar stWorld
   mkAppM ``StateRefT' #[ω, σ, m]

src/Lean/Elab/BuiltinTerm.lean

@@ -18,11 +18,11 @@ namespace Lean.Elab.Term
 open Meta
 
 @[builtin_term_elab «prop»] def elabProp : TermElab := fun _ _ =>
-  return mkSort levelZero
+  return mkSort Level.zero
 
 private def elabOptLevel (stx : Syntax) : TermElabM Level :=
   if stx.isNone then
-    pure levelZero
+    pure Level.zero
   else
     elabLevel stx[0]
 

src/Lean/Elab/Command.lean

@@ -754,10 +754,10 @@ def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
           if xs.all (·.isFVar) then
             Term.withoutAutoBoundImplicit <| elabFn xs
           else
-            -- Abstract any mvars that appear in `xs` using `mkForallFVars` (the type `mkSort levelZero` is an arbitrary placeholder)
+            -- Abstract any mvars that appear in `xs` using `mkForallFVars` (the type `mkSort Level.zero` is an arbitrary placeholder)
             -- and then rebuild the local context from scratch.
             -- Resetting prevents the local context from including the original fvars from `xs`.
-            let ctxType ← Meta.mkForallFVars' xs (mkSort levelZero)
+            let ctxType ← Meta.mkForallFVars' xs (mkSort Level.zero)
             Meta.withLCtx {} {} <| Meta.forallBoundedTelescope ctxType xs.size fun xs _ =>
               Term.withoutAutoBoundImplicit <| elabFn xs
 

src/Lean/Elab/DeclNameGen.lean

@@ -95,8 +95,8 @@ private partial def winnowExpr (e : Expr) : MetaM Expr := do
           visit (body.instantiate1 arg)
     | .letE _n _t v b _ => visit (b.instantiate1 v)
     | .sort .. =>
-      if e.isProp then return .sort levelZero
-      else if e.isType then return .sort levelOne
+      if e.isProp then return .sort Level.zero
+      else if e.isType then return .sort Level.one
       else return .sort (.param `u)
     | .const name .. => return .const name []
     | .mdata _ e' => visit e'

src/Lean/Elab/Deriving/DecEq.lean

@@ -249,7 +249,7 @@ def mkEnumOfNatThm (declName : Name) : MetaM Unit := do
   withLocalDeclD `x enumType fun x => do
     let resultType := mkApp2 eqEnum (mkApp ofNat (mkApp ctorIdx x)) x
     let motive     ← mkLambdaFVars #[x] resultType
-    let casesOn    := mkConst (mkCasesOnName declName) (levelZero :: levels)
+    let casesOn    := mkConst (mkCasesOnName declName) (Level.zero :: levels)
     let mut value  := mkApp2 casesOn motive x
     for ctor in ctors do
       value := mkApp value (mkApp rflEnum (mkConst ctor levels))

src/Lean/Elab/Extra.lean

@@ -546,7 +546,7 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
       let mut maxType := r.max?.get!
       /- If `noProp == true` and `maxType` is `Prop`, then set `maxType := Bool`. `See toBoolIfNecessary` -/
       if noProp then
-        if (← withNewMCtxDepth <| isDefEq maxType (mkSort levelZero)) then
+        if (← withNewMCtxDepth <| isDefEq maxType (mkSort Level.zero)) then
           maxType := Lean.mkConst ``Bool
       let result ← toExprCore (← applyCoe tree maxType (isPred := true))
       trace[Elab.binrel] "result: {result}"
@@ -557,7 +557,7 @@ where
   toBoolIfNecessary (e : Expr) : TermElabM Expr := do
     if noProp then
       -- We use `withNewMCtxDepth` to make sure metavariables are not assigned
-      if (← withNewMCtxDepth <| isDefEq (← inferType e) (mkSort levelZero)) then
+      if (← withNewMCtxDepth <| isDefEq (← inferType e) (mkSort Level.zero)) then
         return (← ensureHasType (Lean.mkConst ``Bool) e)
     return e
 

src/Lean/Elab/MutualInductive.lean

@@ -737,7 +737,7 @@ private partial def simplifyResultingUniverse (u : Level) (paramConst := false)
     -- If there's a variable, then these dominate at infinity; constants can be eliminated
     if (acc.any fun l _ => varies l) then acc.filter (fun l _ => varies l) else acc
   let germMax (acc : LevelMap Nat) : Level :=
-    (simpAcc acc).fold (init := levelZero) fun u l offset => mkLevelMax' u (l.addOffset offset)
+    (simpAcc acc).fold (init := Level.zero) fun u l offset => mkLevelMax' u (l.addOffset offset)
   let accInsert (acc : LevelMap Nat) (u : Level) (offset : Nat) : LevelMap Nat :=
     acc.alter u (fun offset? => some (max (offset?.getD 0) offset))
   -- Simplifies `u+offset`, accumulating `max` arguments in `acc`.
@@ -748,7 +748,7 @@ private partial def simplifyResultingUniverse (u : Level) (paramConst := false)
     | .max a b => simp b offset (simp a offset acc)
     | .imax a b =>
       if b.isAlwaysZero then
-        accInsert acc levelZero offset
+        accInsert acc Level.zero offset
       else if a.isAlwaysZero || b.isNeverZero then
         simp b offset (simp a offset acc)
       else
@@ -796,7 +796,7 @@ private structure AccLevelState where
   /--
   The constraint `u ≤ ?r + k` is represented by `levels[u] := k`.
   When `k` is negative, this represents `u + (-k) ≤ ?r`.
-  The level `u` is either a parameter, metavariable, or `levelZero`.
+  The level `u` is either a parameter, metavariable, or `Level.zero`.
 
   When `k ≥ 0`, this is potentially a "bad" level constraint.
   -/
@@ -951,8 +951,8 @@ private def inferResultingUniverse (views : Array InductiveView)
   -- For `Prop` candidates, need to examine `u` itself, rather than `univForInfer` (which has been simplified).
   if let Level.mvar mvarId := u.normalize then
     if ← isPropCandidate numParams indTypes indFVars then
-      -- May as well assign now, since `levelZero` is already normalized.
-      assignLevelMVar mvarId levelZero
+      -- May as well assign now, since `Level.zero` is already normalized.
+      assignLevelMVar mvarId Level.zero
       return { u := u, assign? := none }
   -- Proceed with non-`Prop`-candidate case.
   let univForInfer ← withViewTypeRef views <| processResultingUniverseForInference u
@@ -975,13 +975,13 @@ private def inferResultingUniverse (views : Array InductiveView)
       (l, k) :: parts
   trace[Elab.inductive] "inferResultingUniverse r: {r}, rOffset: {rOffset}, rConstraints: {rConstraints}"
   /- Compute the inferred `r` -/
-  let rInferred := Level.normalize <| rConstraints.foldl (init := levelZero) fun u' (level, k) =>
+  let rInferred := Level.normalize <| rConstraints.foldl (init := Level.zero) fun u' (level, k) =>
     -- If `k ≤ 0`, then add `level + (-k) ≤ ?r` constraint, otherwise add `level ≤ ?r`.
     mkLevelMax' u' <| level.addOffset (-k).toNat
   let uInferred := (u.replace fun v => if v == r then some rInferred else none).normalize
   /- Analyze "bad" constraints if there are any, and report an error if needed. -/
   if rConstraints.any (fun (_, k) => k > 0) then
-    let uAtZero := u.replace fun v => if v == r then some levelZero else none
+    let uAtZero := u.replace fun v => if v == r then some Level.zero else none
     /- For "bad" level constraints (those of the form `l ≤ ?r + k` where `k > 0`),
     we add `rOffset - k` to both sides to get the ideal constraint. -/
     let uIdeal := Level.normalize <| rConstraints.foldl (init := uAtZero) fun u' (level, k) =>

src/Lean/Elab/PreDefinition/Main.lean

@@ -67,7 +67,7 @@ private def setLevelMVarsAtPreDef (preDef : PreDefinition) : PreDefinition :=
     let value' :=
       preDef.value.replaceLevel fun l =>
         match l with
-        | .mvar _ => levelZero
+        | .mvar _ => Level.zero
         | _       => none
     { preDef with value := value' }
   else

src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean

@@ -104,7 +104,7 @@ def IndGroupInst.nestedTypeFormers (igi : IndGroupInst) : MetaM (Array Expr) :=
   assert! recInfo.numMotives = igi.numMotives
   let lvls :=
     if igi.levels.length = recInfo.levelParams.length then igi.levels
-    else levelZero :: igi.levels
+    else Level.zero :: igi.levels
   let aux := mkAppN (.const recName lvls) igi.params
   let motives ← inferArgumentTypesN recInfo.numMotives aux
   let auxMotives : Array Expr := motives[igi.all.size...*]

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -434,9 +434,9 @@ instance : ToFormat GuessLexRel where
 
 /-- Given a `GuessLexRel`, produce a binary `Expr` that relates two `Nat` values accordingly. -/
 def GuessLexRel.toNatRel : GuessLexRel → Expr
-  | lt => mkAppN (mkConst ``LT.lt [levelZero]) #[mkConst ``Nat, mkConst ``instLTNat]
-  | eq => mkAppN (mkConst ``Eq [levelOne]) #[mkConst ``Nat]
-  | le => mkAppN (mkConst ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat]
+  | lt => mkAppN (mkConst ``LT.lt [Level.zero]) #[mkConst ``Nat, mkConst ``instLTNat]
+  | eq => mkAppN (mkConst ``Eq [Level.one]) #[mkConst ``Nat]
+  | le => mkAppN (mkConst ``LE.le [Level.zero]) #[mkConst ``Nat, mkConst ``instLENat]
   | no_idea => unreachable!
 
 /--

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean

@@ -26,7 +26,7 @@ def mkType (w : Expr) : Expr := mkApp (.const ``BitVec []) w
 def mkInstMul (w : Expr) : Expr := mkApp (.const ``BitVec.instMul []) w
 
 def mkInstHMul (w : Expr) : Expr :=
-  mkApp2 (mkConst ``instHMul [levelZero]) (BitVec.mkType w) (mkInstMul w)
+  mkApp2 (mkConst ``instHMul [Level.zero]) (BitVec.mkType w) (mkInstMul w)
 
 end BitVec
 

src/Lean/Expr.lean

@@ -723,7 +723,7 @@ def mkInstOfNatNat (n : Expr) : Expr :=
   mkApp (mkConst ``instOfNatNat) n
 
 def mkNatLitCore (n : Expr) : Expr :=
-  mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst ``Nat) n (mkInstOfNatNat n)
+  mkApp3 (mkConst ``OfNat.ofNat [Level.zero]) (mkConst ``Nat) n (mkInstOfNatNat n)
 
 /--
 Returns a natural number literal used in the frontend. It is a `OfNat.ofNat` application.
@@ -867,7 +867,7 @@ Return `true` if the given expression is a free variable with the given id.
 Examples:
 - `isFVarOf (.fvar id) id` is `true`
 - ``isFVarOf (.fvar id) id'`` is `false`
-- ``isFVarOf (.sort levelZero) id`` is `false`
+- ``isFVarOf (.sort Level.zero) id`` is `false`
 -/
 def isFVarOf : Expr → FVarId → Bool
   | .fvar fvarId, fvarId' => fvarId == fvarId'
@@ -1175,7 +1175,7 @@ private def getAppArgsAux : Expr → Array Expr → Nat → Array Expr
 
 /-- Given `f a₁ a₂ ... aₙ`, returns `#[a₁, ..., aₙ]` -/
 @[inline] def getAppArgs (e : Expr) : Array Expr :=
-  let dummy := mkSort levelZero
+  let dummy := mkSort Level.zero
   let nargs := e.getAppNumArgs
   getAppArgsAux e (.replicate nargs dummy) (nargs-1)
 
@@ -1190,7 +1190,7 @@ In particular, given `f a₁ a₂ ... aₙ`, returns `#[aₖ₊₁, ..., aₙ]`
 where `k` is minimal such that the size of this array is at most `maxArgs`.
 -/
 @[inline] def getBoundedAppArgs (maxArgs : Nat) (e : Expr) : Array Expr :=
-  let dummy := mkSort levelZero
+  let dummy := mkSort Level.zero
   let nargs := min maxArgs e.getAppNumArgs
   getBoundedAppArgsAux e (.replicate nargs dummy) nargs
 
@@ -1208,7 +1208,7 @@ private def getAppRevArgsAux : Expr → Array Expr → Array Expr
 
 /-- Given `e = f a₁ a₂ ... aₙ`, returns `k f #[a₁, ..., aₙ]`. -/
 @[inline] def withApp (e : Expr) (k : Expr → Array Expr → α) : α :=
-  let dummy := mkSort levelZero
+  let dummy := mkSort Level.zero
   let nargs := e.getAppNumArgs
   withAppAux k e (.replicate nargs dummy) (nargs-1)
 
@@ -1222,7 +1222,7 @@ Note that `f` may be an application.
 The resulting array has size `n` even if `f.getAppNumArgs < n`.
 -/
 @[inline] def getAppArgsN (e : Expr) (n : Nat) : Array Expr :=
-  let dummy := mkSort levelZero
+  let dummy := mkSort Level.zero
   loop n e (.replicate n dummy)
 where
   loop : Nat → Expr → Array Expr → Array Expr
@@ -2179,23 +2179,23 @@ namespace Nat
 protected def mkType : Expr := mkConst ``Nat
 
 def mkInstAdd : Expr := mkConst ``instAddNat
-def mkInstHAdd : Expr := mkApp2 (mkConst ``instHAdd [levelZero]) Nat.mkType mkInstAdd
+def mkInstHAdd : Expr := mkApp2 (mkConst ``instHAdd [Level.zero]) Nat.mkType mkInstAdd
 
 def mkInstSub : Expr := mkConst ``instSubNat
-def mkInstHSub : Expr := mkApp2 (mkConst ``instHSub [levelZero]) Nat.mkType mkInstSub
+def mkInstHSub : Expr := mkApp2 (mkConst ``instHSub [Level.zero]) Nat.mkType mkInstSub
 
 def mkInstMul : Expr := mkConst ``instMulNat
-def mkInstHMul : Expr := mkApp2 (mkConst ``instHMul [levelZero]) Nat.mkType mkInstMul
+def mkInstHMul : Expr := mkApp2 (mkConst ``instHMul [Level.zero]) Nat.mkType mkInstMul
 
 def mkInstDiv : Expr := mkConst ``Nat.instDiv
-def mkInstHDiv : Expr := mkApp2 (mkConst ``instHDiv [levelZero]) Nat.mkType mkInstDiv
+def mkInstHDiv : Expr := mkApp2 (mkConst ``instHDiv [Level.zero]) Nat.mkType mkInstDiv
 
 def mkInstMod : Expr := mkConst ``Nat.instMod
-def mkInstHMod : Expr := mkApp2 (mkConst ``instHMod [levelZero]) Nat.mkType mkInstMod
+def mkInstHMod : Expr := mkApp2 (mkConst ``instHMod [Level.zero]) Nat.mkType mkInstMod
 
 def mkInstNatPow : Expr := mkConst ``instNatPowNat
-def mkInstPow  : Expr := mkApp2 (mkConst ``instPowNat [levelZero]) Nat.mkType mkInstNatPow
-def mkInstHPow : Expr := mkApp3 (mkConst ``instHPow [levelZero, levelZero]) Nat.mkType Nat.mkType mkInstPow
+def mkInstPow  : Expr := mkApp2 (mkConst ``instPowNat [Level.zero]) Nat.mkType mkInstNatPow
+def mkInstHPow : Expr := mkApp3 (mkConst ``instHPow [Level.zero, Level.zero]) Nat.mkType Nat.mkType mkInstPow
 
 def mkInstLT : Expr := mkConst ``instLTNat
 def mkInstLE : Expr := mkConst ``instLENat
@@ -2261,23 +2261,23 @@ protected def mkType : Expr := mkConst ``Int
 def mkInstNeg : Expr := mkConst ``Int.instNegInt
 
 def mkInstAdd : Expr := mkConst ``Int.instAdd
-def mkInstHAdd : Expr := mkApp2 (mkConst ``instHAdd [levelZero]) Int.mkType mkInstAdd
+def mkInstHAdd : Expr := mkApp2 (mkConst ``instHAdd [Level.zero]) Int.mkType mkInstAdd
 
 def mkInstSub : Expr := mkConst ``Int.instSub
-def mkInstHSub : Expr := mkApp2 (mkConst ``instHSub [levelZero]) Int.mkType mkInstSub
+def mkInstHSub : Expr := mkApp2 (mkConst ``instHSub [Level.zero]) Int.mkType mkInstSub
 
 def mkInstMul : Expr := mkConst ``Int.instMul
-def mkInstHMul : Expr := mkApp2 (mkConst ``instHMul [levelZero]) Int.mkType mkInstMul
+def mkInstHMul : Expr := mkApp2 (mkConst ``instHMul [Level.zero]) Int.mkType mkInstMul
 
 def mkInstDiv : Expr := mkConst ``Int.instDiv
-def mkInstHDiv : Expr := mkApp2 (mkConst ``instHDiv [levelZero]) Int.mkType mkInstDiv
+def mkInstHDiv : Expr := mkApp2 (mkConst ``instHDiv [Level.zero]) Int.mkType mkInstDiv
 
 def mkInstMod : Expr := mkConst ``Int.instMod
-def mkInstHMod : Expr := mkApp2 (mkConst ``instHMod [levelZero]) Int.mkType mkInstMod
+def mkInstHMod : Expr := mkApp2 (mkConst ``instHMod [Level.zero]) Int.mkType mkInstMod
 
 def mkInstPow : Expr := mkConst ``Int.instNatPow
-def mkInstPowNat  : Expr := mkApp2 (mkConst ``instPowNat [levelZero]) Int.mkType mkInstPow
-def mkInstHPow : Expr := mkApp3 (mkConst ``instHPow [levelZero, levelZero]) Int.mkType Nat.mkType mkInstPowNat
+def mkInstPowNat  : Expr := mkApp2 (mkConst ``instPowNat [Level.zero]) Int.mkType mkInstPow
+def mkInstHPow : Expr := mkApp3 (mkConst ``instHPow [Level.zero, Level.zero]) Int.mkType Nat.mkType mkInstPowNat
 
 def mkInstLT : Expr := mkConst ``Int.instLTInt
 def mkInstLE : Expr := mkConst ``Int.instLEInt
@@ -2369,17 +2369,17 @@ def mkIntDvd (a b : Expr) : Expr :=
 
 def mkIntLit (n : Int) : Expr :=
   let r := mkRawNatLit n.natAbs
-  let r := mkApp3 (mkConst ``OfNat.ofNat [levelZero]) Int.mkType r (mkApp (mkConst ``instOfNat) r)
+  let r := mkApp3 (mkConst ``OfNat.ofNat [Level.zero]) Int.mkType r (mkApp (mkConst ``instOfNat) r)
   if n < 0 then
     mkIntNeg r
   else
     r
 
 def reflBoolTrue : Expr :=
-  mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)
+  mkApp2 (mkConst ``Eq.refl [Level.one]) (mkConst ``Bool) (mkConst ``Bool.true)
 
 def reflBoolFalse : Expr :=
-  mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.false)
+  mkApp2 (mkConst ``Eq.refl [Level.one]) (mkConst ``Bool) (mkConst ``Bool.false)
 
 def eagerReflBoolTrue : Expr :=
   mkApp2 (mkConst ``eagerReduce [0]) (mkApp3 (mkConst ``Eq [1]) (mkConst ``Bool) (mkConst ``Bool.true) (mkConst ``Bool.true)) reflBoolTrue

src/Lean/Level.lean

@@ -129,8 +129,8 @@ def hasParam (u : Level) : Bool :=
 
 end Level
 
-@[expose, implicit_reducible] def levelZero :=
-  Level.zero
+@[deprecated Level.zero (since := "2026-02-27")] -- This was previously required in order to get the computed field `data` to work, but it is no longer needed.
+abbrev levelZero := Level.zero
 
 def mkLevelMVar (mvarId : LMVarId) :=
   Level.mvar mvarId
@@ -147,9 +147,12 @@ def mkLevelMax (u v : Level) :=
 def mkLevelIMax (u v : Level) :=
   Level.imax u v
 
-def levelOne := mkLevelSucc levelZero
+abbrev Level.one := mkLevelSucc .zero
 
-@[export lean_level_mk_zero] def mkLevelZeroEx : Unit → Level := fun _ => levelZero
+@[deprecated Level.one (since := "2026-02-27")]
+abbrev levelOne := Level.one
+
+@[export lean_level_mk_zero] def mkLevelZeroEx : Unit → Level := fun _ => .zero
 @[export lean_level_mk_succ] def mkLevelSuccEx : Level → Level := mkLevelSucc
 @[export lean_level_mk_mvar] def mkLevelMVarEx : LMVarId → Level := mkLevelMVar
 @[export lean_level_mk_param] def mkLevelParamEx : Name → Level := mkLevelParam
@@ -214,7 +217,7 @@ def isAlwaysZero : Level → Bool
   | imax _  l₂   => isAlwaysZero l₂
 
 @[expose, implicit_reducible] def ofNat : Nat → Level
-  | 0   => levelZero
+  | 0   => Level.zero
   | n+1 => mkLevelSucc (ofNat n)
 
 instance instOfNat (n : Nat) : OfNat Level n where
@@ -388,7 +391,7 @@ partial def normalize (l : Level) : Level :=
       let lvl₁  := lvls[i]!
       let prev  := lvl₁.getLevelOffset
       let prevK := lvl₁.getOffset
-      mkMaxAux lvls k (i+1) prev prevK levelZero
+      mkMaxAux lvls k (i+1) prev prevK Level.zero
     | imax l₁ l₂ =>
       if l₂.isNeverZero then addOffset (normalize (mkLevelMax l₁ l₂)) k
       else
@@ -580,7 +583,7 @@ def updateIMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level :=
   | _        => panic! "imax level expected"
 
 def mkNaryMax : List Level → Level
-  | []    => levelZero
+  | []    => Level.zero
   | [u]   => u
   | u::us => mkLevelMax' u (mkNaryMax us)
 

src/Lean/Meta/AppBuilder.lean

@@ -26,7 +26,7 @@ def mkExpectedTypeHintCore (e : Expr) (expectedType : Expr) (expectedTypeUniv :
 Given `proof` s.t. `inferType proof` is definitionally equal to `expectedProp`, returns
 term `@id expectedProp proof`. -/
 def mkExpectedPropHint (proof : Expr) (expectedProp : Expr) : Expr :=
-  mkExpectedTypeHintCore proof expectedProp levelZero
+  mkExpectedTypeHintCore proof expectedProp Level.zero
 
 /--
 Given `e` s.t. `inferType e` is definitionally equal to `expectedType`, returns

src/Lean/Meta/Basic.lean

@@ -2293,7 +2293,7 @@ Return `true` if `indVal` is an inductive predicate. That is, `inductive` type i
 def isInductivePredicateVal (indVal : InductiveVal) : MetaM Bool := do
   forallTelescopeReducing indVal.type fun _ type => do
     match (← whnfD type) with
-    | .sort u .. => return u == levelZero
+    | .sort u .. => return u == Level.zero
     | _ => return false
 
 /--

src/Lean/Meta/Constructions/CtorIdx.lean

@@ -65,7 +65,7 @@ public def mkCtorIdx (indName : Name) : MetaM Unit :=
           pure (mkRawNatLit 0)
         else
           let motive ← mkLambdaFVars (indices.push x) natType
-          let mut value := mkConst casesOnName (levelOne::us)
+          let mut value := mkConst casesOnName (Level.one::us)
           value := mkAppN value params
           value := mkApp value motive
           value := mkAppN value indices

src/Lean/Meta/IndPredBelow.lean

@@ -186,7 +186,7 @@ def mkBRecOn (ctx : Context) : MetaM Unit := do
   withBRecOnArgs (ctx := ctx) fun newMinors proofArgs => do
     let nmotives := ctx.motives.size
     let lparams := ctx.levelParams.map Level.param
-    let lparams := if ctx.largeElim then levelZero :: lparams else lparams
+    let lparams := if ctx.largeElim then Level.zero :: lparams else lparams
     for i in *...nmotives do
       let motive := ctx.motives[i]!
       let motiveType ← inferType motive