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

Equations

• Lean.mkBelow declName = Lean.mkBelowOrIBelow declName true

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

Equations

• Lean.mkIBelow declName = Lean.mkBelowOrIBelow declName false

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

Equations

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

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

Equations

• Lean.mkBRecOn declName = Lean.mkBRecOnOrBInductionOn declName false

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

Equations

• Lean.mkBInductionOn declName = Lean.mkBRecOnOrBInductionOn declName true