Zulip Chat Archive

Stream: general

Topic: docstrings in widgets

Johan Commelin (Nov 16 2021 at 08:40):

How hard would it be to render docstrings in the widget popups?

Gabriel Ebner (Nov 16 2021 at 09:37):

In Lean 4 we already have them:

Gabriel Ebner (Nov 16 2021 at 09:38):

For Lean 3, I believe we would need add it here: https://github.com/leanprover-community/mathlib/blob/30abde680b4585860610162bcf73136c3b0b2d8c/src/tactic/interactive_expr.lean#L285

Last updated: Aug 03 2023 at 10:10 UTC