fix: expose ctorIdx and per-constructor elims (#10301)

This PR exposes ctorIdx and per-constructor eliminators. Fixes #10299.

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
 
 
 /--

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

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update
+
 namespace lean {
 options get_default_options() {
     options opts;

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