core / init.meta.widget.interactive_expr
eformat but without any of the formatting stuff like highlighting, groups etc.
Make an interactive expression.
Render the implicit arguments for an expression in fancy, little pills.
A group of local constants in the context that should be rendered as one line.
Group consecutive locals according to whether they have the same type
Component that displays the main (first) goal.
Component that displays all goals, together with the $n goals message.
Component that displays the term-mode goal.
Widget used to display term-proof goals.