mathlib documentation

core.init.meta.widget.tactic_component

meta def widget.tc  :
Type → Type → 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 widget.tc.of_component {π α : Type} :
widget.component «π» αwidget.tc «π» α

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

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

meta def widget.tc.mk_simple {π α : Type} [decidable_eq «π»] (β σ : Type) :
(«π» → tactic «σ»)(«π» → «σ» → β → tactic («σ» × option α))(«π» → «σ» → 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.

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

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

meta def widget.tc.to_component {α : Type} :
widget.tc unit αwidget.component tactic_state α

@[instance]
meta def widget.tc.cfn {π α : Type} :