def Lean.Meta.elimOptParam (type : Lean.Expr) : Lean.CoreM Lean.Expr

Equations

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

def Lean.Meta.mkInjectiveTheoremNameFor (ctorName : Lean.Name) : Lean.Name

Equations

• Lean.Meta.mkInjectiveTheoremNameFor ctorName = ctorName ++ Lean.Name.mkStr1 "inj"

def Lean.Meta.mkInjectiveEqTheoremNameFor (ctorName : Lean.Name) : Lean.Name

Equations

• Lean.Meta.mkInjectiveEqTheoremNameFor ctorName = ctorName ++ Lean.Name.mkStr1 "injEq"

opaque Lean.Meta.genInjectivity : Lean.Option Bool

def Lean.Meta.mkInjectiveTheorems (declName : Lean.Name) : Lean.MetaM Unit

Equations

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