opaque Lean.Meta.pp.auxDecls : Lean.Option Bool

opaque Lean.Meta.pp.implementationDetailHyps : Lean.Option Bool

opaque Lean.Meta.pp.inaccessibleNames : Lean.Option Bool

opaque Lean.Meta.pp.showLetValues : Lean.Option Bool

def Lean.Meta.getGoalPrefix (mvarDecl : MetavarDecl) : String

Equations

• Lean.Meta.getGoalPrefix mvarDecl = if (Lean.isLHSGoal? mvarDecl.type).isSome = true then "| " else "⊢ "

def Lean.Meta.ppGoal (mvarId : MVarId) : MetaM Format

Equations

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

def Lean.Meta.ppGoal.pushPending (indent : Int) (ids : List Name) (type? : Option Expr) (fmt : Format) : MetaM Format

Equations

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

def Lean.Meta.ppGoal.ppVars (indent : Int) (showLetValues : Bool) (varNames : List Name) (prevType? : Option Expr) (fmt : Format) (localDecl : LocalDecl) : MetaM (List Name × Option Expr × Format)

Equations

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