TLA+ Lecture Series - possible mistake

[John Calcote]

Hi, 

In the TLA+ video tutorial series, Lecture 7, at time offset 3:43, the following is given:

Maximum(S) == IF S = {} THEN -1

                                             ELSE smallest number in S

I believe this should say "largest number in S". If not, please explain why "smallest" is appropriate here. The math that follows describes a search for the largest number in S.

Note Dr. Lamport's verbal treatise in the video also mentions "smallest number in S".

Perhaps this was modified from an earlier version of the video where the formula was called Minimum(S)? 

Kindest regards,

John

[John Calcote]

Ok - I just found the errata sheet and it already mentions that correction. Sorry for the noise.