mathlib documentation

tactic.explode_widget

#explode_widget command #

Render a widget that displays an #explode proof, providing more interactivity such as jumping to definitions and exploding constants occurring in the exploded proofs.

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

Redefine some of the style attributes for better formatting.

source
meta def tactic.explode_widget.insert_explode {γ : Type} :
expr → tactic (list (widget.html (widget_override.interactive_expression.action γ)))

Explode button for subsequent exploding.

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

Render a subexpression as a list of html elements.

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

Make an interactive expression.

source
meta def tactic.explode_widget.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 tactic.explode_widget.type_tooltip  :
widget.tc subexpr empty

Component for the type tooltip.

source
meta def tactic.explode_widget.show_type_component  :
widget.tc expr empty

Component that shows a type.

source
meta def tactic.explode_widget.show_constant_component  :
widget.tc expr empty

Component that shows a constant.

source
meta def tactic.explode_widget.lookup_lines  :
tactic.explode.entries → ℕ → tactic.explode.entry

Search for an entry that has the specified line number.

source
meta def tactic.explode_widget.goal_row (e : expr) (show_expr : bool := tt) :
tactic (list (widget.html empty))

Render a row that shows a goal.

source
meta def tactic.explode_widget.id_row {γ : Type} (l : ℕ) :
tactic (list (widget.html γ))

Render a row that shows the ID of a goal.

source
meta def tactic.explode_widget.rule_row  :
tactic.explode.thm → tactic (list (widget.html empty))

Render a row that shows the rule or theorem being applied.

source
meta def tactic.explode_widget.proof_row {γ : Type} (args : list (widget.html γ)) :
list (widget.html γ)

Render a row that contains the sub-proofs, i.e., the proofs of the arguments.

source
meta def tactic.explode_widget.assemble_table {γ : Type} (gr ir rr : list (widget.html γ)) :
list (widget.html γ) → widget.html γ

Combine the goal row, id row, rule row and proof row to make them a table.

source
meta def tactic.explode_widget.assemble (es : tactic.explode.entries) :
tactic.explode.entry → tactic (widget.html empty)

Render a table for a given entry.

source
meta def tactic.explode_widget.explode_component (es : tactic.explode.entries) :
tactic (widget.html empty)

Render a widget from given entries.

source
meta def tactic.explode_widget.explode_entries (n : name) (hide_non_prop : bool := tt) :
tactic tactic.explode.entries

Explode a theorem and return entries.

source
meta def tactic.explode_widget_cmd (_x : interactive.parse (lean.parser.tk "#explode_widget")) :
lean.parser unit

User command of the explode widget.