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
  • 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
    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 "_") :
          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
              source
              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.
              Instances For