Documentation

Lean.Meta.Tactic.Grind.PP

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

Helper function for pretty printing the state for debugging purposes.

Equations
    Instances For
      source
      def Lean.Meta.Grind.ppENodeRef (e : Expr) :
      GoalM MessageData

      Helper function for pretty printing the state for debugging purposes.

      Equations
        Instances For
          source
          def Lean.Meta.Grind.Goal.ppState (goal : Goal) :
          MetaM MessageData

          Pretty print goal state for debugging purposes.

          Equations
            Instances For
              source
              def Lean.Meta.Grind.ppGoals (goals : List Goal) :
              MetaM MessageData
              Equations
                Instances For
                  source
                  def Lean.Meta.Grind.ppExprArray (cls : Name) (header : String) (es : Array Expr) (clsElem : Name := Name.mkSimple "_") :
                  MessageData
                  Equations
                    Instances For
                      source
                      def Lean.Meta.Grind.goalToMessageData (goal : Goal) (config : Grind.Config) :
                      MetaM MessageData
                      Equations
                        Instances For
                          source
                          def Lean.Meta.Grind.goalToMessageData.go (goal : Goal) (config : Grind.Config) :
                          Lean.Meta.Grind.M✝ Unit
                          Equations
                            Instances For