HepLean 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.splitGoalsAndGetNth (nth : Nat) (reverse : optParam Bool false) :
Lean.Elab.Tactic.TacticM (Lean.MVarId × List Lean.MVarId × List Lean.MVarId)

If the current goals are g₁ ⋯ gᵢ ⋯ gₙ, splitGoalsAndGetNth i returns (gᵢ, [g₁, ⋯, gᵢ₋₁], [gᵢ₊₁, ⋯, gₙ]).

If reverse is passed as true, the i-th goal is picked by counting backwards. For instance, splitGoalsAndGetNth 1 true puts the last goal in the first component of the returned term.

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 Tactic.rotate_goals, which moves 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.

        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