Documentation

Lean.Meta.Tactic.Grind.SearchM

A choice (aka backtracking) point in the search tree.

  • goalPending : Goal

    Goal where the case-split was performed. Invariant: goalOld.mvarId is not assigned.

  • proof : Expr

    Expression to be assigned to goalOld.mvarId if it is not possible to perform non-chronological backtracking. proof is often a casesOn application containing meta-variables.

  • todo : List Goal

    Subgoals that still need to be processed.

  • generation : Nat
Instances For
    Equations
    Instances For
      Equations
      Instances For
        Equations
        Instances For
          @[reducible, inline]
          Equations
          Instances For
            @[reducible, inline]
            abbrev Lean.Meta.Grind.liftGoalM {α : Type} (x : GoalM α) :
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[inline]
              def Lean.Meta.Grind.SearchM.run {α : Type} (goal : Goal) (x : SearchM α) :
              Equations
              Instances For
                def Lean.Meta.Grind.mkChoice (proof : Expr) (subgoals : List Goal) (generation : Nat) :

                Given a proof containing meta-variables corresponding to the given subgoals, create a choice point.

                • If there are no choice points, we just close the current goal using proof.
                • If there is only one subgoal s, we close the current goal using proof, and update current goal using s.
                • If there are more than one s :: ss, we create a choice point using the current goal as the pending goal, and update the current goal with s.
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Create an auxiliary metavariable with the same type and tag of the metavariable associated with the current goal. We use this function to perform cases on the current goal without eagerly assignining it.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Select the next goal to be processed from the choiceStack. This function assumes the current goal has been closed (i.e., inconsistent is true) Returns some gen if a new goal was found for a choice point with generation gen, and returns none otherwise.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For