def Lean.Meta.Grind.Goal.ppENodeRef (goal : Goal) (e : Expr) : MetaM MessageData

Helper function for pretty printing the state for debugging purposes.

def Lean.Meta.Grind.ppENodeRef (e : Expr) : GoalM MessageData

Helper function for pretty printing the state for debugging purposes.

def Lean.Meta.Grind.Goal.ppState (goal : Goal) : MetaM MessageData

Pretty print goal state for debugging purposes.

def Lean.Meta.Grind.ppGoals (goals : List Goal) : MetaM MessageData

def Lean.Meta.Grind.ppExprArray (cls : Name) (header : String) (es : Array Expr) (clsElem : Name := Name.mkSimple "_") (collapsed : Bool := true) : MessageData

Functions for deciding whether an expression is a support application or not when displaying equivalence classes. This is hard-coded for now. We will probably make it extensible in the future.

def Lean.Meta.Grind.isSupportApp (e : Expr) : MetaM Bool

Returns true if e is a support-like application. Recall that equivalence classes that contain only support applications are displayed in the "others" category.

def Lean.Meta.Grind.ppEqc (eqc : List Expr) (children : Array MessageData := #[]) : MessageData

def Lean.Meta.Grind.Arith.Cutsat.pp? (goal : Goal) : MetaM (Option MessageData)

def Lean.Meta.Grind.goalDiagToMessageData (goal : Goal) (config : Grind.Config) (header : String := "Goal diagnostics") (collapsedMain : Bool := true) : MetaM MessageData

def Lean.Meta.Grind.goalToMessageData (goal : Goal) (config : Grind.Config) : MetaM MessageData