mathlib documentation

core / init.meta.widget.tactic_component

meta def (π α : Type) :

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

meta def {π α : Type} :
widget.component «π» α «π» α
meta def {π α β : Type} (f : α → β) : «π» α «π» β
meta def {π ρ α : Type} (f : «π» → ρ) : ρ α «π» α
meta def {π α : 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 {π α : Type} [decidable_eq «π»] (view : «π» → tactic (list (widget.html α))) : «π» α
meta def {π α : Type} : «π» α«π» → tactic (widget.html α)
meta def {α : Type} : unit αwidget.component tactic_state α
@[protected, instance]
meta def {π α : Type} :
has_coe_to_fun ( «π» α) (λ (x : «π» α), «π» → tactic (widget.html α))