Documentation

Lean.Meta.AbstractNestedProofs

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Meta.abstractNestedProofs (mainDeclName : Name) (e : Expr) :

Replace proofs nested in e with new lemmas. The new lemmas have names of the form mainDeclName.proof_<idx>

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