hwayne / learntla

A TLA+ guide
http://www.learntla.com
Creative Commons Attribution 4.0 International
278 stars 57 forks source link

About the with behavior on set containing duplicated elements #80

Closed PineWu closed 5 years ago

PineWu commented 5 years ago

When performing on set containing duplicated elements, I found that with only creates a behavior for each distinct element in the set. with a \in {1, 1, 2,2, 3,3} do print a; end with The output will be: 1, 2, 3 Is my understanding right? If so, I think it's better to emphasize this behavior.

hwayne commented 5 years ago

That's because sets only consist of unique elements. try putting {1, 1, 1, 1, 1, 1} into the evaluator: it should output {1}.

PineWu commented 5 years ago

That's because sets only consist of unique elements. try putting {1, 1, 1, 1, 1, 1} into the evaluator: it should output {1}.

Got it. Thanks much~