A tactic stub file for the guard_goal_nums tactic.

ink

def guardGoalNums : Lean.ParserDescr

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

Equations

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