Documentation

Lean.Meta.AbstractNestedProofs

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Instances For
      @[inline, reducible]
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        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.
        Instances For