def Lean.mkCtorIdxName (indName : Name) : Name

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

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

def Lean.mkCtorIdx (indName : Name) : 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.