mathlib3 documentation


#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.

@[protected, instance]
meta def widget.string_to_html {α : Type} :
has_coe string (widget.html α)

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 {γ : Type} (tooltip : subexpr γ) :

Make an interactive expression.

meta def tactic.explode_widget.implicit_arg_list (tooltip : 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 := :
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.