count_heartbeats!_In__ — Mathlib

Lean4
/-- `#count_heartbeats! in tac` runs a tactic 10 times, counting the heartbeats used, and logs the range
and standard deviation. The tactic `#count_heartbeats! n in tac` runs it `n` times instead.
-/
@[tactic_parser 1000]
public meta def «tactic#count_heartbeats!_In__» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.CountHeartbeats.«tactic#count_heartbeats!_In__» 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "#count_heartbeats! " false✝)
            (ParserDescr.unary✝ `optional (ParserDescr.const✝ `num)))
          (ParserDescr.symbol✝ "in"))
        (ParserDescr.unary✝ `group (ParserDescr.const✝ `ppLine)))
      (ParserDescr.const✝ `tacticSeq))
Похожие утверждения