learning_tla/learn_tla/core/01-operators-and-values.md

1. Operators and values

CHOOSE

Selects one value from the set of all those matching a set, like:

ToClock(seconds) == 
  CHOOSE x \in ClockType: 
    ToSeconds(x) = seconds

If multiple values satisfy CHOOSE, the theoretical requirement is that the result be deterministic. In practice, TLC will always choose the lowest value matching the set.