mathlib3 documentation

core / init.meta.widget.html_cmd

source
meta def show_widget_cmd (x : interactive.parse (lean.parser.tk "#html")) :
lean.parser unit

Accepts terms with the type component tactic_state empty or html empty and renders them interactively.