clarification on EXCEPT

[cwlucas41]

the except section includes:

What we actually wanted to write is that s' is the same as s except that s[1] is false. Here’s the syntax for that:

Next == s' = [s EXCEPT ![1] = FALSE]

Yes, I know it’s really awkward. No, I can’t think of anything better.

Could you clarify why the ! is necessary? To me it seems like a double-negative as I read the line in my head as "the sequence s except that not the the first index has value is FALSE". On first reading I actually expected this to modify index 2+ (all indexes not the first) due to the ! and would have thought that [s EXCEPT [1] = FALSE] would do as intended.

I found the text explaining how you think about the colon earlier very useful for being able to read the code better.

I’ve found that the best way to remember which is which is by reading the colon as a “where”. So the map is “x squared where x in 1..4”, while the filter is “x in 1..4 where x is even”.

How do you think about the meaning of Next == s' = [s EXCEPT ![1] = FALSE]?

[cwlucas41]

Ah, silly me ! isn't a NOT operator here so this makes sense. Maybe helping clarify what ! is would help. I had to go to the very dense manual to learn that it is a positional selector.

[hwayne]

I didn't see this until now and you're right I should clarify