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.

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.