search

hwayne / learntla-v2

Learn TLA+ for free! No prior experience necessary!
https://www.learntla.com
Other
185 stars 39 forks source link

Question about > vs. = in example. #5

Closed th closed 1 year ago

th commented 2 years ago

operators.rst:

{t \in ClockType: t[2] = 29 /\ t[3] = 0}

Why not t[2] = 30? We're 1-indexing, right?

At first I misunderstood that as “all the times in the second half of the hour” and wondered why there isn't a > anywhere. Maybe check if others misread it similarly?

hwayne commented 2 years ago

This is 0-indexing (minutes go from 0 to 59). will fix.

hwayne commented 1 year ago

Fixed