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
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Lean.Meta.ppGoal.pushPending (indent : Int) (ids : List Name) (type? : Option Expr) (fmt : Format) :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Lean.Meta.ppGoal.ppVars (indent : Int) (tactic : Bool) (varNames : List Name) (prevType? : Option Expr) (fmt : Format) (localDecl : LocalDecl) :
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For