Rocq-style goal selectors

n: tac, 1,3-5: tac, all: tac — apply a tactic sequence to a chosen range of subgoals, and the matching form in conv.

def CustomPrelude.Tactic.range_selector.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.range_selector : Category

Equations

• Lean.Parser.Category.range_selector = { }

def CustomPrelude.Tactic.range_selector_ : Lean.ParserDescr

Equations

• CustomPrelude.Tactic.range_selector_ = Lean.ParserDescr.node `CustomPrelude.Tactic.range_selector_ 1022 (Lean.ParserDescr.const `num)

def CustomPrelude.Tactic.«range_selector_-_» : Lean.ParserDescr

Equations

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

def CustomPrelude.Tactic.tac_selector.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.tac_selector : Category

Equations

• Lean.Parser.Category.tac_selector = { }

def CustomPrelude.Tactic.tac_selector_ : Lean.ParserDescr

Select multiple ranges of subgoals.

Equations

• CustomPrelude.Tactic.tac_selector_ = Lean.ParserDescr.node `CustomPrelude.Tactic.tac_selector_ 1022 ((Lean.ParserDescr.cat `range_selector 0).sepBy1 "," (Lean.ParserDescr.symbol ", "))

def CustomPrelude.Tactic.tac_selectorAll : Lean.ParserDescr

Select all the subgoals.

Equations

• CustomPrelude.Tactic.tac_selectorAll = Lean.ParserDescr.node `CustomPrelude.Tactic.tac_selectorAll 1024 (Lean.ParserDescr.symbol "all")

def CustomPrelude.Tactic.«tactic_:_» : Lean.ParserDescr

Select the subgoals onto which to apply a given tactic sequence, Rocq style.

Equations

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

def CustomPrelude.Tactic.«conv_:_» : Lean.ParserDescr

Select the subgoals onto which to apply a given conv sequence, Rocq style.

Equations

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