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.

Redefine some of the style attributes for better formatting.

Explode button for subsequent exploding.

Render a subexpression as a list of html elements.

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

Make an interactive expression.

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.

Component for the type tooltip.

Component that shows a type.

Component that shows a constant.

Search for an entry that has the specified line number.

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.

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

Render a row that shows the ID of a goal.

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

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.

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.

Render a table for a given entry.

Render a widget from given entries.

Explode a theorem and return entries.

User command of the explode widget.