A tactic stub file for the guard_goal_nums tactic.

def guardGoalNums : Lean.ParserDescr

guard_goal_nums n succeeds if there are exactly n goals and fails otherwise.

Equations

• guardGoalNums = Lean.ParserDescr.node `guardGoalNums 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "guard_goal_nums " false) (Lean.ParserDescr.const `num))