Documentation

Lean.Meta.Tactic.Grind.Solve

source
def Lean.Meta.Grind.tryFallback :
GoalM Bool
Equations
    Instances For
      source
      def Lean.Meta.Grind.solve (goal : Goal) :
      GrindM (Option Goal)

      Try to solve/close the given goal. Returns some goal if this subgoal failed to be closed, and none if all subgoals were closed.

      Equations
        Instances For
          source
          def Lean.Meta.Grind.solve.main :
          SearchM (Option Goal)
          Equations
            Instances For
              source
              def Lean.Meta.Grind.solve.loop :
              SearchM (Option Goal)
              Equations
                Instances For