Documentation

Lean.Meta.Tactic.Grind.Inv

Debugging support code for checking basic invariants.

source
def Lean.Meta.Grind.checkChild (e child : Expr) :
GoalM Bool
Equations
    Instances For
      source
      def Lean.Meta.Grind.checkInvariants (expensive : Bool := false) :
      GoalM Unit

      Checks basic invariants if grind.debug is enabled.

      Equations
        Instances For
          source
          def Lean.Meta.Grind.Goal.checkInvariants (goal : Goal) (expensive : Bool := false) :
          GrindM Unit
          Equations
            Instances For