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 "_") : MessageData

Equations

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

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.

def Lean.Meta.Grind.goalToMessageData.go (goal : Goal) (config : Grind.Config) : Lean.Meta.Grind.M✝ Unit

Equations

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