Documentation

Lean.Meta.PPGoal

source
opaque Lean.Meta.pp.auxDecls :
Lean.Option Bool
source
opaque Lean.Meta.pp.implementationDetailHyps :
Lean.Option Bool
source
opaque Lean.Meta.pp.inaccessibleNames :
Lean.Option Bool
source
opaque Lean.Meta.pp.showLetValues :
Lean.Option Bool
source
def Lean.Meta.getGoalPrefix (mvarDecl : Lean.MetavarDecl) :
String
Instances For
    source
    def Lean.Meta.ppGoal (mvarId : Lean.MVarId) :
    Lean.MetaM Lean.Format
    Instances For
      source
      def Lean.Meta.ppGoal.pushPending (indent : Int) (ids : List Lake.Name) (type? : Option Lean.Expr) (fmt : Lean.Format) :
      Lean.MetaM Lean.Format
      Instances For
        source
        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)
        Instances For