commandExtend_docs__Before__After_

Lean4
/-- `extend_docs <declName> before <prefix_string> after <suffix_string>` extends the
docs of `<declName>` by adding `<prefix_string>` before and `<suffix_string>` after. -/
@[command_parser 1000]
public meta def commandExtend_docs__Before__After_ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.ExtendDocs.commandExtend_docs__Before__After_ 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "extend_docs") (ParserDescr.const✝ `ident))
        (ParserDescr.unary✝ `optional
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `colGt)
              ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "before " false✝))
            (ParserDescr.const✝ `str))))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `colGt)
            ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "after " false✝))
          (ParserDescr.const✝ `str))))
Похожие утверждения