Lean4
/-- `guard_hyp_nums n` succeeds if there are exactly `n` hypotheses and fails otherwise.
Note that, depending on what options are set, some hypotheses in the local context might
not be printed in the goal view. This tactic computes the total number of hypotheses,
not the number of visible hypotheses.
-/
@[tactic_parser 1000]
public meta def guardHypNums : Lean.ParserDescr✝ :=
ParserDescr.node✝ `guardHypNums 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "guard_hyp_nums " false✝) (ParserDescr.const✝ `num))