← Copula mathematical handbook

def Lean.Meta.mkCtorIdxHInjTheoremNameFor (indName : Name) : Name

Equations

• Lean.Meta.mkCtorIdxHInjTheoremNameFor indName = (Lean.mkCtorIdxName indName).str Lean.Meta.hinjSuffix✝