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 : Lean.MetavarDecl) : String

Equations

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

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

Equations

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

def Lean.Meta.ppGoal.pushPending (indent : Int) (ids : List Lake.Name) (type? : Option Lean.Expr) (fmt : Lean.Format) : Lean.MetaM Lean.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 Lake.Name) (prevType? : Option Lean.Expr) (fmt : Lean.Format) (localDecl : Lean.LocalDecl) : Lean.MetaM (List Lake.Name × Option Lean.Expr × Lean.Format)

Equations

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