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.
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.