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.

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

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