guardHypNums

Mathlib.Tactic.GuardHypNums

URI: https://scilib.ai/kg/mathlib#guardHypNums

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))

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru