mathlib3 documentation

core / init.meta.widget.interactive_expr

meta def subexpr  :
meta def widget.interactive_expression.mk {γ : Type} (tooltip : widget.tc subexpr γ) :

Make an interactive expression.

Render the implicit arguments for an expression in fancy, little pills.

meta inductive widget.filter_type  :
meta structure widget.local_collection  :

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.

meta def widget.tactic_view_component {γ : Type} (local_c : widget.tc widget.local_collection γ) (target_c : widget.tc expr γ) :

Component that displays all goals, together with the $n goals message.

meta def widget.tactic_view_term_goal {γ : Type} (local_c : widget.tc widget.local_collection γ) (target_c : widget.tc expr γ) :

Component that displays the term-mode goal.

meta def widget.tactic_state_widget  :
widget.component tactic_state empty
meta def widget.term_goal_widget  :
widget.component tactic_state empty

Widget used to display term-proof goals.