Docs

Small helpers for surfacing docstrings in the InfoView.

This is intentionally available through the widget entrypoint (import NN.Entrypoint.Widgets) or directly as import NN.Widgets.Core.Docs, since it depends on ProofWidgets.

Commands:

• #tl_doc f prints the type + docstring for f as an info message.
• #tl_doc_view f renders the type + docstring for f as a rich HTML panel in the InfoView.

Tip: if you already have an identifier in the InfoView (e.g. under “Expected type”), you can also hover it to see its type + docstring. InfoView hover tooltips can be toggled in VS Code under Lean 4 > Infoview: Show Tooltip On Hover.

Main definitions

• #tl_doc f: print f's type and docstring in a plain info message.
• #tl_doc_view f: show the same information in a richer HTML panel.

Implementation notes

• We intentionally keep the command surface small: in day-to-day work, one "quick text" and one "richer panel" mode is usually enough.
• We resolve terms to constants before lookup, because that keeps behavior predictable and avoids surprising partial reductions.
• We use ProofWidgets #html so this stays a Lean-native widget (no external JS pipeline).

References

• Lean metaprogramming book
• Lean community documentation style
• ProofWidgets examples

Tags

docs, infoview, proofwidgets, metaprogramming, developer-tools

def NN.Widgets.DocsInternal.preWrap (s : String) : ProofWidgets.Html

def NN.Widgets.DocsInternal.docPanel (declName typeStr docStr : String) : ProofWidgets.Html

def NN.Widgets.DocsInternal.termConstName? (e : Lean.Expr) : Option Lean.Name

Return the head constant name of an application, if one exists.

def NN.Widgets.DocsInternal.renderDocString (doc? : Option String) : String

Normalize optional docs into user-facing text.

def NN.Widgets.DocsInternal.ppConstType (n : Lean.Name) : Lean.Elab.Command.CommandElabM String

Pretty-print a declaration type using Lean's normal pretty-printer.

def NN.Widgets.DocsInternal.resolveConstFromTerm (t : Lean.Syntax) : Lean.Elab.Command.CommandElabM Lean.Name

Resolve an input term to a declaration name for doc lookup.

Commands

def NN.Widgets.tlDocCmd : Lean.ParserDescr

def NN.Widgets.tlDocViewCmd : Lean.ParserDescr