refactor: make .ctorIdx not an abbrev (#11644)

This PR makes `.ctorIdx` not an abbrev; we don't want `grind` to unfold
it.

src/Lean/Meta/Constructions/CtorIdx.lean

@@ -71,17 +71,17 @@ public def mkCtorIdx (indName : Name) : MetaM Unit :=
             value := mkApp value alt
           pure value
         mkLambdaFVars (xs.push x) value
+      let hints := ReducibilityHints.regular (getMaxHeight (← getEnv) declValue + 1)
       let decl := .defnDecl (← mkDefinitionValInferringUnsafe
         (name        := declName)
         (levelParams := info.levelParams)
         (type        := declType)
         (value       := declValue)
-        (hints       := ReducibilityHints.abbrev)
+        (hints       := hints)
       )
       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

stage0/src/stdlib_flags.h

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

tests/lean/run/ctorIdx.lean

@@ -2,7 +2,7 @@ inductive Enum where | a1 | a2 | a3 | a4 | a5
 deriving DecidableEq
 
 /--
-info: @[reducible] protected def Enum.ctorIdx : Enum → Nat :=
+info: protected def Enum.ctorIdx : Enum → Nat :=
 fun x => Enum.casesOn x 0 1 2 3 4
 -/
 #guard_msgs in
@@ -11,7 +11,7 @@ fun x => Enum.casesOn x 0 1 2 3 4
 inductive NonRec where | a1 (u : Unit) | a2 (i : Int) | a3 (n : Nat) (f : Fin n) | a4 (s : String) (b : Bool) | a5
 
 /--
-info: @[reducible] protected def NonRec.ctorIdx : NonRec → Nat :=
+info: protected def NonRec.ctorIdx : NonRec → Nat :=
 fun x => NonRec.casesOn x (fun u => 0) (fun i => 1) (fun n f => 2) (fun s b => 3) 4
 -/
 #guard_msgs in
@@ -24,7 +24,7 @@ inductive Nested (α : Type) where
   | a3 (z : List (Nested α))
 
 /--
-info: @[reducible] protected def Nested.ctorIdx : {α : Type} → Nested α → Nat :=
+info: protected def Nested.ctorIdx : {α : Type} → Nested α → Nat :=
 fun {α} x => x.casesOn (fun x => 0) (fun y => 1) fun z => 2
 -/
 #guard_msgs in
@@ -42,13 +42,13 @@ inductive B (m : Nat) : Nat → Type
 end
 
 /--
-info: @[reducible] protected def A.ctorIdx : {m a : Nat} → A m a → Nat :=
+info: protected def A.ctorIdx : {m a : Nat} → A m a → Nat :=
 fun {m a} x => x.casesOn (fun {n} a => 0) (fun {n} a => 1) 2
 -/
 #guard_msgs in
 #print A.ctorIdx
 /--
-info: @[reducible] protected def B.ctorIdx : {m a : Nat} → B m a → Nat :=
+info: protected def B.ctorIdx : {m a : Nat} → B m a → Nat :=
 fun {m a} x => x.casesOn (fun {n} a => 0) (fun {n} a => 1) 2
 -/
 #guard_msgs in
@@ -58,7 +58,7 @@ fun {m a} x => x.casesOn (fun {n} a => 0) (fun {n} a => 1) 2
 
 inductive Single where | only (n : Nat)
 /--
-info: @[reducible] protected def Single.ctorIdx : Single → Nat :=
+info: protected def Single.ctorIdx : Single → Nat :=
 fun x => 0
 -/
 #guard_msgs in #print Single.ctorIdx
@@ -67,7 +67,7 @@ structure Struct where
   field1 : Nat
   field2 : Bool
 /--
-info: @[reducible] protected def Struct.ctorIdx : Struct → Nat :=
+info: protected def Struct.ctorIdx : Struct → Nat :=
 fun x => 0
 -/
 #guard_msgs in #print Struct.ctorIdx
@@ -76,7 +76,7 @@ fun x => 0
 
 unsafe inductive U : Type | mk : (U → U) → U
 /--
-info: @[reducible] unsafe protected def U.ctorIdx : U → Nat :=
+info: unsafe protected def U.ctorIdx : U → Nat :=
 fun x => 0
 -/
 #guard_msgs in