Documentation

Mathlib.Tactic.GuardHypNums

A tactic stub file for the guard_hyp_nums tactic.

def guardHypNums :
Lean.ParserDescr

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.

Instances For