Zulip Chat Archive

Stream: general

Topic: Attaching docstrings within mathlib to things from lean core


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Sep 11 2020 at 21:40):

Using tools that are part of mathlib

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Sep 14 2020 at 10:53):

Attempted in #4144


Last updated: May 06 2021 at 22:13 UTC