def Lean.mkBelow (declName : Name) : MetaM Unit

Equations

• Lean.mkBelow declName = Lean.mkBelowOrIBelow✝ declName true

def Lean.mkIBelow (declName : Name) : MetaM Unit

Equations

• Lean.mkIBelow declName = Lean.mkBelowOrIBelow✝ declName false

def Lean.mkBRecOnOrBInductionOn (indName : Name) (ind : Bool) : MetaM Unit

Equations

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

def Lean.mkBRecOn (declName : Name) : MetaM Unit

Equations

• Lean.mkBRecOn declName = Lean.mkBRecOnOrBInductionOn declName false

def Lean.mkBInductionOn (declName : Name) : MetaM Unit

Equations

• Lean.mkBInductionOn declName = Lean.mkBRecOnOrBInductionOn declName true