registerHintStx — Mathlib

Lean4
/-- Register a tactic for use with the `hint` tactic, e.g. `register_hint simp_all`.
An optional priority can be provided with `register_hint (priority := n) tac`.
Tactics with larger priorities run before those with smaller priorities. The default
priority is `1000`.
-/
@[command_parser 1000]
public meta def registerHintStx : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.Hint.registerHintStx 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "register_hint")
        (ParserDescr.unary✝ `optional
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen
              (ParserDescr.binary✝ `andthen
                (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "(") (ParserDescr.symbol✝ "priority"))
                (ParserDescr.symbol✝ ":="))
              (ParserDescr.const✝ `num))
            (ParserDescr.symbol✝ ")"))))
      (ParserDescr.cat✝ `tactic 0))
Похожие утверждения