mathlib documentation

tactic.interactive_expr

Widgets used for tactic state and term-mode goal display

The vscode extension supports the display of interactive widgets. Default implementation of these widgets are included in the core library. We override them here using vm_override so that we can change them quickly without waiting for the next Lean release.

The function widget_override.interactive_expression.mk renders a single expression as a widget component. Each goal in a tactic state is rendered using the widget_override.tactic_view_goal function, a complete tactic state is rendered using widget_override.tactic_view_component.

Lean itself calls the widget_override.term_goal_widget function to render term-mode goals and widget_override.tactic_state_widget to render the tactic state in a tactic proof.

Prints a debugging representation of an sf object.

Constructs an sf from an eformat by forgetting grouping, nesting, etc.

Post-process an sf object to eliminate tags for partial applications by pushing the app_fn as far into the expression as possible. The effect is that clicking on a sub-expression always includes the full argument list in the popup.

Consider the expression id id 0. We push the app_fn for the partial application id id inwards and eliminate it. Before:

(tag_expr [app_fn]
  `(id.{1} (nat -> nat) (id.{1} nat))
  (tag_expr [app_fn] `(id.{1} (nat -> nat)) "id")
  "\n"
  (tag_expr [app_arg] `(id.{1} nat) "id"))
"\n"
(tag_expr [app_arg] `(has_zero.zero.{0} nat nat.has_zero) "0")

After:

"id"
"\n"
(tag_expr [app_fn, app_arg] `(id.{1} nat) "id")
"\n"
(tag_expr [app_arg] `(has_zero.zero.{0} nat nat.has_zero) "0")
meta inductive widget_override.interactive_expression.action  :
Type → Type

The actions accepted by an expression widget.

Render a 'go to definition' button for a given expression. If there is no definition available, then returns an empty list.

Due to a bug in the webview browser, we have to reduce the number of spans in the expression. To do this, we collect the attributes from sf.block and sf.highlight after an expression boundary.

Make an interactive expression.

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

meta inductive widget_override.filter_type  :
Type

Supported tactic state filters.

Filters a local constant using the given filter.

Component for the filter dropdown.

meta def widget_override.html.of_name {α : Type} :
namewidget.html α

Converts a name into an html element.

Component that shows a type.

meta structure widget_override.local_collection  :
Type

A group of local constants in the context that should be rendered as one line.

Converts a single local constant into a (singleton) local_collection

Component that displays the main (first) goal.

meta inductive widget_override.tactic_view_action  :
Type → Type

Actions accepted by the tactic_view_component.

meta def widget_override.goals_accomplished_message {α : Type} :
widget.html α

The "goals accomplished 🎉" HTML widget. This can be overridden using:

meta def my_new_msg {α : Type} : widget.html α := "my message"
attribute [vm_override my_new_msg] widget_override.goals_accomplished_message

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

Component that displays the term-mode goal.

Renders the current tactic state.

Component showing the current tactic state.

meta def widget_override.term_goal_widget  :
widget.component tactic_state empty

Widget used to display term-proof goals.