- tag_expr : expr.address → expr → widget.interactive_expression.sf → widget.interactive_expression.sf
- compose : widget.interactive_expression.sf → widget.interactive_expression.sf → widget.interactive_expression.sf
- of_string : string → widget.interactive_expression.sf
eformat but without any of the formatting stuff like highlighting, groups etc.
- on_mouse_enter : Π (γ : Type), subexpr → widget.interactive_expression.action γ
- on_mouse_leave_all : Π (γ : Type), widget.interactive_expression.action γ
- on_click : Π (γ : Type), subexpr → widget.interactive_expression.action γ
- on_tooltip_action : Π (γ : Type), γ → widget.interactive_expression.action γ
- on_close_tooltip : Π (γ : Type), widget.interactive_expression.action γ
def
widget.interactive_expression.view
{γ : Type} :
widget.tc subexpr (widget.interactive_expression.action γ) → option expr.address → option expr.address → subexpr → widget.interactive_expression.sf → tactic (list (widget.html (widget.interactive_expression.action γ)))
- none : widget.filter_type
- no_instances : widget.filter_type
- only_props : widget.filter_type
@[instance]
Group consecutive locals according to whether they have the same type
Component that displays the main (first) goal.
- out : Π (γ : Type), γ → widget.tactic_view_action γ
- filter : Π (γ : Type), widget.filter_type → widget.tactic_view_action γ
Component that displays all goals, together with the $n goals message.
Component that displays the term-mode goal.
Widget used to display term-proof goals.