feat: deprecate .toCtorIdx for .ctorIdx (#10113)

This PR deprecates `.toCtorIdx` for the more naturally named `.ctorIdx`
(and updates the standard library).

src/Init/Data/Ord/Basic.lean

@@ -531,7 +531,7 @@ instance [Ord α] : Ord (Option α) where
   | some x, some y => compare x y
 
 instance : Ord Ordering where
-  compare := compareOn (·.toCtorIdx)
+  compare := compareOn (·.ctorIdx)
 
 namespace List
 

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -33,7 +33,7 @@ inductive CompletionItemKind where
   deriving Inhabited, DecidableEq, Repr, Hashable
 
 instance : ToJson CompletionItemKind where
-  toJson a := toJson (a.toCtorIdx + 1)
+  toJson a := toJson (a.ctorIdx + 1)
 
 instance : FromJson CompletionItemKind where
   fromJson? v := do
@@ -51,7 +51,7 @@ inductive CompletionItemTag where
   deriving Inhabited, DecidableEq, Repr, Hashable
 
 instance : ToJson CompletionItemTag where
-  toJson t := toJson (t.toCtorIdx + 1)
+  toJson t := toJson (t.ctorIdx + 1)
 
 instance : FromJson CompletionItemTag where
   fromJson? v := do
@@ -352,7 +352,7 @@ def SemanticTokenType.names : Array String :=
     "regexp", "operator", "decorator", "leanSorryLike"]
 
 def SemanticTokenType.toNat (tokenType : SemanticTokenType) : Nat :=
-  tokenType.toCtorIdx
+  tokenType.ctorIdx
 
 -- sanity check
 example {v : SemanticTokenType} : open SemanticTokenType in
@@ -383,7 +383,7 @@ def SemanticTokenModifier.names : Array String :=
     "async", "modification", "documentation", "defaultLibrary"]
 
 def SemanticTokenModifier.toNat (modifier : SemanticTokenModifier) : Nat :=
-  modifier.toCtorIdx
+  modifier.ctorIdx
 
 -- sanity check
 example {v : SemanticTokenModifier} : open SemanticTokenModifier in

src/Lean/Elab/Binders.lean

@@ -14,6 +14,7 @@ public import Lean.Elab.PreDefinition.TerminationHint
 public import Lean.Elab.Match
 public import Lean.Compiler.MetaAttr
 meta import Lean.Parser.Term
+import Lean.Linter.Basic
 
 public section
 

src/Lean/Elab/Deriving/BEq.lean

@@ -130,7 +130,7 @@ private def mkBEqEnumFun (ctx : Context) (name : Name) : TermElabM Syntax := do
   let auxFunName := ctx.auxFunNames[0]!
   let vis := ctx.mkVisibilityFromTypes
   let expAttr := ctx.mkNoExposeAttrFromCtors
-  `(@[$[$expAttr],*] $vis:visibility def $(mkIdent auxFunName):ident  (x y : $(mkCIdent name)) : Bool := x.toCtorIdx == y.toCtorIdx)
+  `(@[$[$expAttr],*] $vis:visibility def $(mkIdent auxFunName):ident  (x y : $(mkCIdent name)) : Bool := x.ctorIdx == y.ctorIdx)
 
 private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do
   let ctx ← mkContext "beq" name

src/Lean/Elab/Deriving/DecEq.lean

@@ -186,7 +186,7 @@ def mkDecEqEnum (declName : Name) : CommandElabM Unit := do
     let vis := ctx.mkVisibilityFromTypes
     `($vis:visibility instance : DecidableEq $(mkCIdent declName) :=
         fun x y =>
-          if h : x.toCtorIdx = y.toCtorIdx then
+          if h : x.ctorIdx = y.ctorIdx then
             -- We use `rfl` in the following proof because the first script fails for unit-like datatypes due to etaStruct.
             isTrue (by first | have aux := congrArg $ofNatIdent h; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl)
           else

src/Lean/Elab/Inductive.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Elab.MutualInductive
+import Lean.Linter.Basic
 
 public section
 

src/Lean/Elab/Structure.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Meta.Structure
 public import Lean.Elab.MutualInductive
+import Lean.Linter.Basic
 
 public section
 

src/Lean/Elab/Tactic/Lets.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Tactic.Lets
 public import Lean.Elab.Tactic.Location
 import Lean.Elab.Binders
+import Lean.Linter.Basic
 
 public section
 

src/Lean/Environment.lean

@@ -1913,7 +1913,7 @@ private def ImportedModule.publicModule? (self : ImportedModule) : Option Module
 private def ImportedModule.getData? (self : ImportedModule) (level : OLeanLevel) : Option ModuleData := do
   -- Without the module system, we only have the exported level.
   let level := if (← self.publicModule?).isModule then level else .exported
-  self.parts[level.toCtorIdx]?.map (·.1)
+  self.parts[level.ctorIdx]?.map (·.1)
 
 /-- The main module data that will eventually be used to construct the kernel environment. -/
 private def ImportedModule.mainModule? (self : ImportedModule) : Option ModuleData :=

src/Lean/Linter/Deprecated.lean

@@ -6,9 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Linter.Basic
-public import Lean.Attributes
-public import Lean.Elab.InfoTree.Main
+public import Lean.Meta.Basic
+import Lean.Linter.Basic
+import Lean.Elab.InfoTree.Main
 
 public section
 
@@ -42,6 +42,12 @@ builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ←
       return { newName?, text?, since? }
   }
 
+def setDeprecated {m} [Monad m] [MonadEnv m] [MonadError m] (declName : Name) (entry : DeprecationEntry) : m Unit := do
+  let env ← getEnv
+  match deprecatedAttr.setParam env declName entry with
+  | Except.ok env   => setEnv env
+  | Except.error ex => throwError ex
+
 def isDeprecated (env : Environment) (declName : Name) : Bool :=
   Option.isSome <| deprecatedAttr.getParam? env declName
 

src/Lean/Linter/List.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Elab.Command
 public import Lean.Server.InfoUtils
+import Lean.Linter.Basic
 
 public section
 set_option linter.missingDocs true -- keep it documented

src/Lean/Meta/Constructions/CtorIdx.lean

@@ -12,6 +12,7 @@ import Lean.AddDecl
 import Lean.Meta.AppBuilder
 import Lean.Meta.CompletionName
 import Lean.Meta.Injective
+import Lean.Linter.Deprecated
 
 open Lean Meta
 
@@ -91,3 +92,4 @@ public def mkCtorIdx (indName : Name) : MetaM Unit := do
       modifyEnv fun env => addToCompletionBlackList env aliasName
       modifyEnv fun env => addProtected env aliasName
       setReducibleAttribute aliasName
+      Lean.Linter.setDeprecated aliasName { newName? := some declName, since? := "2025-08-25" }

tests/lean/run/decEq.lean

@@ -22,7 +22,7 @@ def t2 [DecidableEq α] : DecidableEq (Test α) :=
 /--
 trace: [Elab.Deriving.decEq] ⏎
     public instance : DecidableEq✝ PubEnum✝ := fun x✝ y✝ =>
-      if h✝ : x.toCtorIdx✝ = y.toCtorIdx✝ then
+      if h✝ : x.ctorIdx✝ = y.ctorIdx✝ then
         isTrue✝
           (by
             first