Documentation

Lean.Meta.Tactic.Grind.PP

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

Helper function for pretty printing the state for debugging purposes.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Grind.ppENodeDeclValue (e : Expr) :
GoalM Format

Helper function for pretty printing the state for debugging purposes.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Grind.ppENodeDecl (e : Expr) :
GoalM Format

Helper function for pretty printing the state for debugging purposes.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Grind.ppState :
GoalM Format

Pretty print goal state for debugging purposes.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Grind.ppGoals (goals : List Goal) :
GrindM Format
Equations
  • One or more equations did not get rendered due to their size.