show_kind_ — Mathlib

Lean4
/-- `#show_kind tac` takes as input the syntax of a tactic and returns the `SyntaxNodeKind`
at the head of the tactic syntax tree.

The input syntax needs to parse, though it can be *extremely* elided.
For instance, to see the `SyntaxNodeKind` of the `refine` tactic, you could use
```lean
#show_kind refine _
```
The trailing underscore `_` makes the syntax valid, since `refine` expects something else.
-/
@[command_parser 1000]
public meta def «command#show_kind_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Linter.UnusedTactic.«command#show_kind_» 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#show_kind ") (ParserDescr.cat✝ `tactic 0))
Похожие утверждения