mathlib documentation

core.​init.​meta.​widget.​tactic_component

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} :