structure Lean.Elab.Tactic.Do.ProofMode.MStartResult : Type

• goal : MGoal
• proof? : Option Expr

def Lean.Elab.Tactic.Do.ProofMode.mStart (goal : Expr) : MetaM MStartResult

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.mStartMVar (mvar : MVarId) : MetaM (MVarId × MGoal)

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.elabMStart : Tactic

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.elabMStop : Tactic

Equations

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