Declaration Documentation

#tl_doc f prints a declaration's type and docstring as an info message. #tl_doc_view f renders them in a themed infoview panel. Import NN.Widgets or NN.Widgets.Core.Docs; both commands use Lean's declaration lookup and pretty-printer.

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