def mkToCtorIdxName (indName : Lean.Name) : Lean.Name

def mkCtorIdxName (indName : Lean.Name) : Lean.Name

def isCtorIdxCore? (env : Lean.Environment) (declName : Lean.Name) : Option Lean.InductiveVal

def isCtorIdx? (declName : Lean.Name) : Lean.MetaM (Option Lean.InductiveVal)

def mkCtorIdx (indName : Lean.Name) : Lean.MetaM Unit

For an inductive type T with more than one function builds a function T.ctorIdx : T → Nat that 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.