Lean4
/-- The `#check t` tactic elaborates the term `t` and then pretty prints it with its type as `e : ty`.
If `t` is an identifier, then it pretty prints a type declaration form
for the global constant `t` instead.
Use `#check (t)` to pretty print it as an elaborated expression.
Like the `#check` command, the `#check` tactic allows stuck typeclass instance problems.
These become metavariables in the output.
-/
@[tactic_parser 1000]
public meta def «tactic#check__» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.«tactic#check__» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "#check " false✝)
(ParserDescr.unary✝ `group (ParserDescr.const✝ `colGt)))
(ParserDescr.cat✝ `term 0))
