core / init.meta.widget.tactic_component

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

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

Instances for widget.tc

meta def widget.tc.of_component {π α : Type} :

widget.component π α → widget.tc π α

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

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

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

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

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

meta def widget.tc.to_html {π α : Type} :

widget.tc π α → π → tactic (widget.html α)

meta def widget.tc.to_component {α : Type} :

@[protected, instance]

meta def widget.tc.has_coe_to_fun {π α : Type} :

has_coe_to_fun (widget.tc π α) (λ (x : widget.tc π α), π → tactic (widget.html α))