A tactic stub file for the guard_hyp_nums tactic.
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.
Equations
- guardHypNums = Lean.ParserDescr.node `guardHypNums 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "guard_hyp_nums " false) (Lean.ParserDescr.const `num))