mathlib documentation


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

meta def {π α β : Type} :
(α → β) «π» α «π» β

meta def {π ρ α : Type} :
(«π» → ρ) ρ α «π» α

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

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

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

meta def {π α : Type} :