Attaching docstrings within mathlib to things from lean core

Stream: general

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Eric Wieser]

Using tools that are part of mathlib

[Johan Commelin]

@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]

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]

Attempted in #4144