itauto! — Mathlib

Lean4
@[inherit_doc itauto, tactic_parser 1000]
public meta def itauto! : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.ITauto.itauto! 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "itauto!" false✝)
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ " *" `token.« *» (ParserDescr.symbol✝ " *"))
          (ParserDescr.unary✝¹ `group
            (ParserDescr.binary✝ `andthen
              (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " [")
                ((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.cat✝ `term 0) ","
                  (ParserDescr.symbol✝ ", ") Bool.false✝))
              (ParserDescr.symbol✝ "]"))))))
Похожие утверждения