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

Helper function for pretty printing the state for debugging purposes.

Equations

• One or more equations did not get rendered due to their size.

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

Helper function for pretty printing the state for debugging purposes.

Equations

• Lean.Meta.Grind.ppENodeRef e = do let __do_lift ← get liftM (__do_lift.ppENodeRef e)

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

Pretty print goal state for debugging purposes.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

rings are the Sym.Arith ring records of the run (see Result.rings). The goal itself stores only the ring solver state.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.goalToMessageData (goal : Goal) (config : Grind.Config) (rings : Array Sym.Arith.CommRing) : MetaM MessageData

Equations

• One or more equations did not get rendered due to their size.