def Lean.findDocString? (env : Environment) (declName : Name) (includeBuiltin : Bool := true) (options : Options := ∅) (currNamespace : Name := Name.anonymous) (openDecls : List OpenDecl := []) : 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.

def Lean.findMarkdownDocString? {m : Type → Type} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadLiftT IO m] (declName : Name) (includeBuiltin : Bool := true) : m (Option String)

Finds the docstring for a name, taking the current namespace and open declarations from the ambient monad. Tactic alternate forms and documentation extensions are taken into account.

Docstrings are rendered with the default options.

Equations

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