From 3e24d5dee867dc834662ae9fc594b13b7774c2ae Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 8 Sep 2025 12:04:19 +0200
Subject: [PATCH] fix: expose ctorIdx and per-constructor elims (#10301)

This PR exposes ctorIdx and per-constructor eliminators. Fixes #10299.
---
 src/Lean/Meta/Constructions/CtorElim.lean | 8 +++++---
 src/Lean/Meta/Constructions/CtorIdx.lean  | 3 ++-
 stage0/src/stdlib_flags.h                 | 2 ++
 tests/lean/run/issue10299.lean            | 7 +++++++
 4 files changed, 16 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/issue10299.lean

diff --git a/src/Lean/Meta/Constructions/CtorElim.lean b/src/Lean/Meta/Constructions/CtorElim.lean
index 6efdd0a755..69943209fd 100644
--- a/src/Lean/Meta/Constructions/CtorElim.lean
+++ b/src/Lean/Meta/Constructions/CtorElim.lean
@@ -223,9 +223,11 @@ public def mkCtorElim (indName : Name) : MetaM Unit := do
   let recInfo ← getConstInfo (mkRecName indName)
   unless recInfo.levelParams.length > indVal.levelParams.length do return
 
-  mkCtorElimType indName
-  mkIndCtorElim indName
-  mkConstructorElim indName
+  -- Expose if indName is not private
+  withExporting (isExporting := ! isPrivateName indName) do
+    mkCtorElimType indName
+    mkIndCtorElim indName
+    mkConstructorElim indName
 
 
 /--
diff --git a/src/Lean/Meta/Constructions/CtorIdx.lean b/src/Lean/Meta/Constructions/CtorIdx.lean
index 6720879be4..f00b0e0746 100644
--- a/src/Lean/Meta/Constructions/CtorIdx.lean
+++ b/src/Lean/Meta/Constructions/CtorIdx.lean
@@ -33,7 +33,8 @@ returns the constructor index of the given value.
 Does nothing if `T` does not eliminate into `Type` or if `T` is unsafe.
 Assumes `T.casesOn` to be defined already.
 -/
-public def mkCtorIdx (indName : Name) : MetaM Unit := do
+public def mkCtorIdx (indName : Name) : MetaM Unit :=
+  withExporting (isExporting := ! isPrivateName indName) do
   prependError m!"failed to construct `T.ctorIdx` for `{.ofConstName indName}`:" do
     unless genCtorIdx.get (← getOptions) do return
     let declName := mkCtorIdxName indName
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..d8fc746d3a 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/issue10299.lean b/tests/lean/run/issue10299.lean
new file mode 100644
index 0000000000..05fe025a04
--- /dev/null
+++ b/tests/lean/run/issue10299.lean
@@ -0,0 +1,7 @@
+module
+
+/-! Tests that ctorIdx and constructor elims are exposed, i.e. reduce properly -/
+
+example : Nat.ctorIdx 0 = 0 := rfl
+
+example : Nat.succ.elim 1 rfl (fun n => n) = 0 := rfl