structure Control.UpdateSettings (α : Type) : Type

Configuration for an auto-updating cached value. $$\text{UpdateSettings}(\alpha) = \{ \text{interval} : \mathbb{N},\; \text{action} : \text{IO}(\alpha) \}$$

• updateFreq : Nat

  Update interval in microseconds.

• updateAction : IO α

  The IO action to run periodically to refresh the value.

def Control.UpdateSettings.default {α : Type} (action : IO α) : UpdateSettings α

Default settings with 1-second interval.

Equations

• Control.UpdateSettings.default action = { updateAction := action }

structure Control.AutoUpdate (α : Type) : Type

Handle to a running auto-update background task. Provides a getter for the cached value and a stop action.

• get : IO α

  Read the current cached value (non-blocking).

• stop : IO Unit

  Stop the background update task.

def Control.mkAutoUpdate {α : Type} [Inhabited α] (settings : UpdateSettings α) : IO (AutoUpdate α)

Create an auto-updating cached value. Returns an AutoUpdate handle with a non-blocking getter and a stop action.

The background task runs settings.updateAction every settings.updateFreq microseconds and stores the result. Uses a dedicated OS thread to avoid thread pool starvation.

$$\text{mkAutoUpdate} : \text{UpdateSettings}(\alpha) \to \text{IO}(\text{AutoUpdate}(\alpha))$$

Equations

• One or more equations did not get rendered due to their size.