mathlib documentation

core.init.meta.widget.tactic_component

source
meta def widget.tc (π α : Type) :
Type

A component that implicitly depends on tactic_state. For efficiency we always assume that the tactic_state is unchanged between component renderings.

source
meta def widget.tc.of_component {π α : Type} (a : widget.component «π» α) :
widget.tc «π» α

source
meta def widget.tc.map_action {π α β : Type} (f : α → β) (a : widget.tc «π» α) :
widget.tc «π» β

source
meta def widget.tc.map_props {π ρ α : Type} (f : «π» → ρ) (a : widget.tc ρ α) :
widget.tc «π» α

source
meta def widget.tc.mk_simple {π α : Type} [decidable_eq «π»] (β σ : Type) (init : «π» → tactic σ) (update : «π» → σ → β → tactic (σ × option α)) (view : «π» → σ → tactic (list (widget.html β))) :
widget.tc «π» α

Make a tactic component from some init, update, views which are expecting a tactic. The tactic_state never mutates.

source
meta def widget.tc.stateless {π α : Type} [decidable_eq «π»] (view : «π» → tactic (list (widget.html α))) :
widget.tc «π» α

source
meta def widget.tc.to_html {π α : Type} (a : widget.tc «π» α) (a_1 : «π») :
tactic (widget.html α)

source
meta def widget.tc.to_component {α : Type} (a : widget.tc unit α) :
widget.component tactic_state α

source
@[instance]
meta def widget.tc.cfn {π α : Type} :
has_coe_to_fun (widget.tc «π» α)