I like this method of explanation; I think it helps with getting an intuition for how time is implicit in TLA+. Quantifying over t: Time seems like it makes sense once you've introduced quantifiers, and then you can motivate priming as a straightforward followup from that.
Possible typo in the code block after introducing priming; right now it says
Transfer =
some value in 1..=alice:
1. alice' = alice
2. bob' = bob
I like this method of explanation; I think it helps with getting an intuition for how time is implicit in TLA+. Quantifying over
t: Timeseems like it makes sense once you've introduced quantifiers, and then you can motivate priming as a straightforward followup from that.Possible typo in the code block after introducing priming; right now it says
Should that be
?