def Lean.mkCtorElimName (indName : Name) : Name

Equations

• Lean.mkCtorElimName indName = indName.str "ctorElim"

def Lean.mkConstructorElimName (indName conName : Name) : Name

Equations

• Lean.mkConstructorElimName indName conName = Lean.asPrivateAs✝ (conName.str "elim") indName

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

Equations

• One or more equations did not get rendered due to their size.