mathlib documentation

core / init.meta.widget.interactive_expr

meta def subexpr  :
Type
meta inductive widget.interactive_expression.sf  :
Type

eformat but without any of the formatting stuff like highlighting, groups etc.

meta inductive widget.interactive_expression.action (γ : Type) :
Type
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  :
Type
meta structure widget.local_collection  :
Type

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

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

Component that displays the main (first) goal.

meta inductive widget.tactic_view_action (γ : Type) :
Type
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.