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

opaque Lean.Meta.pp.showLetValues.threshold : Lean.Option Nat

opaque Lean.Meta.pp.showLetValues.tactic.threshold : Lean.Option Nat

def Lean.Meta.ppGoal.shouldShowLetValue (tactic : Bool) (e : Expr) : MetaM Bool

Given the current values of the options pp.showLetValues and pp.showLetValues.threshold, determines whether the local let declaration's value should be omitted.

• tactic is whether the goal is for a tactic metavariable. In that case, uses the maximum of pp.showLetValues.tactic.threshold and pp.showLetValues.threshold for the threshold. In tactics, we usually want to see let values. In contrast, for the "expected type" view we usually do not.

Equations

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

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) (tactic : 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.