[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] How does this simple Max(set) implementation work?

I'm going through the examples at learntla.com and one asks to write an operator that finds the maximum value in a set. I did it using the SetReduce operator from somewhere else in the tutorial, but the given answer is simpler:

Max(S) == CHOOSE x \in S : \A y \in S : y <= x

I can't quite "read" this. Since CHOOSE picks any value from the set where the condition is true, it seems like this would return a value from S that is larger than at least one other value, not larger than all other values. What makes it keep going to find the largest value?

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/22f7c06f-1774-4baf-98d6-32bdc244e0c7n%40googlegroups.com.