From 9ce8a062ba969360551b48cecee62d21c8a4693e Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 26 Nov 2025 12:23:00 +0100
Subject: [PATCH] perf: macro_inline ctorIdx for single constructor inductives
 (#11379)

This PR sets `@[macro_inline]` on the (trivial) `.ctorIdx` for inductive
types with one constructor, to reduce the number of symbols generated by
the compiler.
---
 src/Lean/Meta/Constructions/CtorIdx.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Constructions/CtorIdx.lean b/src/Lean/Meta/Constructions/CtorIdx.lean
index 9914f8ea18..561c9ff24f 100644
--- a/src/Lean/Meta/Constructions/CtorIdx.lean
+++ b/src/Lean/Meta/Constructions/CtorIdx.lean
@@ -71,16 +71,20 @@ public def mkCtorIdx (indName : Name) : MetaM Unit :=
             value := mkApp value alt
           pure value
         mkLambdaFVars (xs.push x) value
-      addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
+      let decl := .defnDecl (← mkDefinitionValInferringUnsafe
         (name        := declName)
         (levelParams := info.levelParams)
         (type        := declType)
         (value       := declValue)
         (hints       := ReducibilityHints.abbrev)
-      ))
+      )
+      addDecl decl
       modifyEnv fun env => addToCompletionBlackList env declName
       modifyEnv fun env => addProtected env declName
       setReducibleAttribute declName
+      if info.numCtors = 1 then
+        setInlineAttribute declName .macroInline
+      compileDecl decl
 
       -- Deprecated alias for enumeration types (which used to have `toCtorIdx`)
       if (← isEnumType indName) then