clarification on efficiency of CHOOSE in introduction

[cwlucas41]

the CHOOSE section states:

Here’s another thing we could do:

1. Take the set of all possible clock values.
2. Pick the element in the set that, when converted to seconds, gives us the value.

We don’t do it this way because “the set of all possible clock values” is over 80,000 elements long and doing a find on an 80,000 element list is a waste of resources. But it more closely matches the definition of the conversion, making it more useful for specification. In TLA+ we can write the selection like this:

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

It's unclear to me if doing it this way actually is a waste of resources (maybe implying there is a better way?) or if it is the best practice for doing this type of operation (I'm guessing this is the case from the text).

[hwayne]

Ah, the intention is supposed to be "we don't do it this way in our programming languages", I'll make it clearer what's meant