docstrings in widgets

Stream: general

[Johan Commelin]

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

[Gabriel Ebner]

In Lean 4 we already have them:
widget-docstring.png

[Gabriel Ebner]

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