source
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.

Instances For

source
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)

Instances For

source
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.

Instances For

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

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

Instances For

source
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.

Instances For

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.

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

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

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

Instances For

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

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

Instances For