Documentation

Lean.Meta.PPGoal

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

Equations
    Instances For
      Equations
        Instances For
          Equations
            Instances For
              def Lean.Meta.ppGoal.pushPending (indent : Int) (ids : List Name) (type? : Option Expr) (fmt : Format) :
              Equations
                Instances For
                  def Lean.Meta.ppGoal.ppVars (indent : Int) (tactic : Bool) (varNames : List Name) (prevType? : Option Expr) (fmt : Format) (localDecl : LocalDecl) :
                  Equations
                    Instances For