Docs

Small helpers for surfacing docstrings in the InfoView.

This is available through the widget entrypoint (import NN.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.

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

Monospaced block that wraps long lines instead of scrolling, for signatures and docstrings.

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

One declaration rendered as a card: name, type, and docstring, themed to the editor.

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