def Lean.findDocString? (env : Lean.Environment) (declName : Lake.Name) (includeBuiltin : optParam Bool true) : IO (Option String)

Finds the docstring for a name, taking tactic alternate forms and documentation extensions into account.

Use Lean.findSimpleDocString? to look up the raw docstring without resolving alternate forms or including extensions.

Equations

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