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.

source
@[instance]
meta def widget_override.interactive_expression.has_mem  :
has_mem expr.coord expr.address

source
meta inductive widget_override.interactive_expression.sf  :
Type

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

source
meta def widget_override.interactive_expression.sf.repr (a : widget_override.interactive_expression.sf) :
format

Prints a debugging representation of an sf object.

source
@[instance]
meta def widget_override.interactive_expression.has_to_format  :
has_to_format widget_override.interactive_expression.sf

source
@[instance]
meta def widget_override.interactive_expression.has_to_string  :
has_to_string widget_override.interactive_expression.sf

source
@[instance]
meta def widget_override.interactive_expression.has_repr  :
has_repr widget_override.interactive_expression.sf

source
meta def widget_override.interactive_expression.sf.of_eformat (a : eformat) :
widget_override.interactive_expression.sf

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

source
meta def widget_override.interactive_expression.sf.flatten (a : widget_override.interactive_expression.sf) :
widget_override.interactive_expression.sf

Flattens an sf, i.e. merges adjacent of_string constructors.

source
meta def widget_override.interactive_expression.sf.elim_part_apps (s : widget_override.interactive_expression.sf) :
widget_override.interactive_expression.sf

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")
source
meta inductive widget_override.interactive_expression.action (γ : Type) :
Type

The actions accepted by an expression widget.

source
meta def widget_override.interactive_expression.goto_def_button {γ : Type} (a : expr) :
tactic (list (widget.html (widget_override.interactive_expression.action γ)))

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

source
meta def widget_override.interactive_expression.get_block_attrs {γ : Type} (a : widget_override.interactive_expression.sf) :
tactic (widget_override.interactive_expression.sf × list (widget.attr γ))

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.

source
meta def widget_override.interactive_expression.view {γ : Type} (tooltip_component : widget.tc subexpr (widget_override.interactive_expression.action γ)) (click_address select_address : option expr.address) (a : subexpr) (a_1 : widget_override.interactive_expression.sf) :
tactic (list (widget.html (widget_override.interactive_expression.action γ)))

Renders a subexpression as a list of html elements.

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

Make an interactive expression.

source
meta def widget_override.interactive_expression.implicit_arg_list (tooltip : widget.tc subexpr empty) (e : expr) :
tactic (widget.html empty)

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

source
meta def widget_override.interactive_expression.type_tooltip  :
widget.tc subexpr empty

Component for the type tooltip.

source
meta inductive widget_override.filter_type  :
Type

Supported tactic state filters.

source
@[instance]
meta def widget_override.filter_type.decidable_eq  :
decidable_eq widget_override.filter_type

source
meta def widget_override.filter_local (a : widget_override.filter_type) (a_1 : expr) :
tactic bool

Filters a local constant using the given filter.

source
meta def widget_override.filter_component  :
widget.component widget_override.filter_type widget_override.filter_type

Component for the filter dropdown.

source
meta def widget_override.html.of_name {α : Type} (a : name) :
widget.html α

Converts a name into an html element.

source
meta def widget_override.show_type_component  :
widget.tc expr empty

Component that shows a type.

source
meta structure widget_override.local_collection  :
Type

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

source
@[instance]
meta def widget_override.local_collection.decidable_eq  :
decidable_eq widget_override.local_collection

source
meta def widget_override.to_local_collection (l : expr) :
tactic widget_override.local_collection

Converts a single local constant into a (singleton) local_collection

source
meta def widget_override.group_local_collection (a : list widget_override.local_collection) :
list widget_override.local_collection

Groups consecutive local collections by type

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

Component that displays the main (first) goal.

source
meta inductive widget_override.tactic_view_action (γ : Type) :
Type

Actions accepted by the tactic_view_component.

source
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
source
meta def widget_override.tactic_view_component {γ : Type} (local_c : widget.tc widget_override.local_collection γ) (target_c : widget.tc expr γ) :
widget.tc unit γ

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

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

Component that displays the term-mode goal.

source
meta def widget_override.show_local_collection_component  :
widget.tc widget_override.local_collection empty

Component showing a local collection.

source
meta def widget_override.tactic_render  :
widget.tc unit empty

Renders the current tactic state.

source
meta def widget_override.tactic_state_widget  :
widget.component tactic_state empty

Component showing the current tactic state.

source
meta def widget_override.term_goal_widget  :
widget.component tactic_state empty

Widget used to display term-proof goals.