scilib documentation

core / init.meta.widget.interactive_expr

source
meta def subexpr  :
Type
source
meta inductive widget.interactive_expression.sf  :
Type

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

Instances for widget.interactive_expression.sf
source
meta def widget.interactive_expression.sf.repr  :
widget.interactive_expression.sf → format
source
@[protected, instance]
meta def widget.interactive_expression.sf.has_to_format  :
has_to_format widget.interactive_expression.sf
source
@[protected, instance]
meta def widget.interactive_expression.sf.has_to_string  :
has_to_string widget.interactive_expression.sf
source
@[protected, instance]
meta def widget.interactive_expression.sf.has_repr  :
has_repr widget.interactive_expression.sf
source
meta def widget.interactive_expression.sf.of_eformat  :
eformat → widget.interactive_expression.sf
source
meta def widget.interactive_expression.sf.flatten  :
widget.interactive_expression.sf → widget.interactive_expression.sf
source
meta inductive widget.interactive_expression.action (γ : Type) :
Type
source
meta def widget.interactive_expression.view {γ : Type} (tooltip_component : widget.tc subexpr (widget.interactive_expression.action γ)) (click_address select_address : option expr.address) :
subexpr → widget.interactive_expression.sf → tactic (list (widget.html (widget.interactive_expression.action γ)))
source
meta def widget.interactive_expression.mk {γ : Type} (tooltip : widget.tc subexpr γ) :
widget.tc expr γ

Make an interactive expression.

source
meta def widget.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.interactive_expression.type_tooltip  :
widget.tc subexpr empty
source
meta inductive widget.filter_type  :
Type
source
@[protected, instance]
meta def widget.filter_type.decidable_eq  :
decidable_eq widget.filter_type
source
meta def widget.filter_local  :
widget.filter_type → expr → tactic bool
source
meta def widget.filter_component  :
widget.component widget.filter_type widget.filter_type
source
meta def widget.show_type_component  :
widget.tc expr empty
source
meta structure widget.local_collection  :
Type

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

source
@[protected, instance]
meta def widget.local_collection.decidable_eq  :
decidable_eq widget.local_collection
source
meta def widget.to_local_collection  :
list widget.local_collection → list expr → tactic (list widget.local_collection)

Group consecutive locals according to whether they have the same type

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

Component that displays the main (first) goal.

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

Component that displays the term-mode goal.

source
meta def widget.show_local_collection_component  :
widget.tc widget.local_collection empty
source
meta def widget.tactic_render  :
widget.tc unit empty
source
meta def widget.tactic_state_widget  :
widget.component tactic_state empty
source
meta def widget.term_goal_widget  :
widget.component tactic_state empty

Widget used to display term-proof goals.