mathlib documentation

core / init.meta.widget.html_cmd

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