search

hwayne / learntla-v2

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

Bug in the LET sample sepc #56

Closed gdymind closed 1 year ago

gdymind commented 1 year ago

In LET, it said:

ToClock2(seconds) ==
  LET
    h == seconds \div 3600
    h_left == seconds % 3600
    m == h_left \div 60
    m_left == h_left % 60
    s == m_left \div 60
  IN
    <<h, m, s>>

It should be s == m_left instead of s == m_left \div 60

hwayne commented 1 year ago

Fixed!