hwayne / learntla-v2

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

text seems to silently swap between examples #82

Open keithb-coop opened 6 months ago

keithb-coop commented 6 months ago

On Writing an Invariant seems to switch silently between examples. It start by using "another spec for finding duplicates that also runs without error", the one where is_unique is set to TRUE. But in the later section Testing Duplicates it seems to be taking the example on the page Writing Specifications in which is_unique gets updated. The first five or seven times I read the page Writing an Invariant I was so confused that I came close to giving up on the whole endeavour, feeling that if I'm not smart enough to understand how the text could possibly apply to the example given on that page I've basically got no chance of ever using this tool.