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