# `extend_doc` command #

In a file where declaration `decl` is defined, writing

    extend_doc decl
      before "I will be added as a prefix to the docs of `decl`"
      after "I will be added as a suffix to the docs of `decl`"

does what is probably clear: it extends the doc-string of `decl` by adding the string of `before` at the beginning and the string of `after` at the end.

At least one of `before` and `after` must appear, but either one of them is optional.

source
def Mathlib.Tactic.ExtendDocs.commandExtend_docs__Before__After_ :
Lean.ParserDescr

`extend_docs <declName> before <prefix_string> after <suffix_string>` extends the docs of `<declName>` by adding `<prefix_string>` before and `<suffix_string>` after.

Equations

- One or more equations did not get rendered due to their size.

Instances For