mathlib documentation


meta def subexpr  :

meta inductive widget.interactive_expression.sf  :

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

meta inductive widget.interactive_expression.action  :
Type → Type

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 inductive widget.tactic_view_action  :
Type → Type

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

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.