## Stream: general

### Topic: Attaching docstrings within mathlib to things from lean core

#### Eric Wieser (Sep 11 2020 at 20:58):

Is it possible to attach docstrings to lemmas that do not come from mathlib? It annoys me that none of the tactics in https://leanprover-community.github.io/mathlib_docs/core/init/meta/converter/interactive.html#conv.interactive.find have any documentation.

And I guess the follow-up, is it better to patch on mathlib docstrings after the fact, or edit the lean community fork to add those docstrings?

#### Simon Hudon (Sep 11 2020 at 21:04):

There is a way to do it but you might as well submit PRs to leanprover-community/lean with documentation

#### Eric Wieser (Sep 11 2020 at 21:40):

Ah, reading another thread it looks like because these are tactics they need to be documented differently?

#### Eric Wieser (Sep 11 2020 at 21:40):

Using tools that are part of mathlib

#### Johan Commelin (Sep 12 2020 at 03:27):

@Eric Wieser Such PRs are very much welcomed! The fact that it hasn't been done is purely because we've all got so much stuff on our hands...

#### Bryan Gin-ge Chen (Sep 12 2020 at 03:30):

You can PR doc strings directly to core. If you want to add "tactic doc entries" for core tactics (the little blurs on our tactics page), then you should edit tactic.lean_core_docs.

#### Eric Wieser (Sep 14 2020 at 10:53):

Attempted in #4144

Last updated: May 06 2021 at 22:13 UTC