@[unbox]

structure SpinnerData : Type

A spinner is a set of frames together with an update interval.

• frames : Array String

  The frames of the spinner (which ideally are all of the same size).

• interval : UInt32

  The update interval, in milliseconds.

• all_frames_same_length (f₁ : String) : f₁ ∈ self.frames → ∀ (f₂ : String), f₂ ∈ self.frames → f₁.length = f₂.length

  All frames must take the same amount of space, so the prompt doesn't shift mid-animation.