Documentation

Batteries.Tactic.PermuteGoals

The on_goal, pick_goal, and swap tactics. #

pick_goal n moves the n-th goal to the front. If n is negative this is counted from the back.

on_goal n => tacSeq focuses on the n-th goal and runs a tactic block tacSeq. If tacSeq does not close the goal any resulting subgoals are inserted back into the list of goals. If n is negative this is counted from the back.

swap is a shortcut for pick_goal 2, which interchanges the 1st and 2nd goals.

source
def Batteries.Tactic.goalNum :
Lean.ParserDescr

A number referring to a goal in the tactic state. n refers to the n-th goal from the front, and -n refers to the n-th goal from the bottom.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Batteries.Tactic.elabGoalNum (goalNum : Lean.Syntax) :
    Lean.Elab.Tactic.TacticM Nat

    Turn the given goalNum syntax into a (zero-based) index in the current getGoals list.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Batteries.Tactic.tacticPick_goal_ :
      Lean.ParserDescr

      pick_goal n will move the n-th goal to the front.

      pick_goal -n will move the n-th goal (counting from the bottom) to the front.

      See also rotate_left/rotate_right, which move goals from the front to the back and vice-versa.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Batteries.Tactic.tacticSwap :
        Lean.ParserDescr

        swap is a shortcut for pick_goal 2, which interchanges the 1st and 2nd goals.

        Equations
        Instances For
          source
          def Batteries.Tactic.«tacticOn_goal_=>_» :
          Lean.ParserDescr

          on_goal n => tacSeq creates a block scope for the n-th goal and tries the sequence of tactics tacSeq on it.

          on_goal -n => tacSeq does the same, but the n-th goal is chosen by counting from the bottom.

          on_goal n₁ ... nᵢ => tacSeq runs tacSeq on each of the goals n₁ ... nᵢ separately.

          The goal is not required to be solved and any resulting subgoals are inserted back into the list of goals, replacing the chosen goal.

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