Documentation

Lean.Meta.Injective

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) :

Equations

Lean.Meta.mkInjectiveTheoremNameFor ctorName = ctorName ++ `inj

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

Equations

Lean.Meta.mkInjectiveEqTheoremNameFor ctorName = ctorName ++ `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.