That is interesting, I would have thought that the answer would be syntactically invalid at first glance. But, in thinking about how the EXCEPT operator would be implemented, it probably has no knowledge of what the function's domain is, and simply loops over all of the provided exceptions, applying each one. This leads to a kind of "mutability" of the function, where the subsequent re-definitions build off of the result of the previous one.
[f EXCEPT e1, e2, e3] is just a shorthand for [[[f EXCEPT e1] EXCEPT e2] EXCEPT e3], so each subsequent exception does operate on the result of the previous.
I never read about the EXCEPT operator to this level of depth, so yes, thanks for sharing!
Consider the following _expression_:
LET f == [n \in 0..10 |-> n] IN
[f EXCEPT ![1] = @ + 1, ![1] = @ + 1, ![1] = @ + 1]
Fairly weird, because we're assigning the value of 1 multiple times using its previous value each time. What do you expect the value of the final function on 1 to be? Runtime exception? 2? Turns out it's 4!
Sort of a weird quirk I found when exploring how TLC interprets functions, don't know whether it's a bug necessarily but thought people might find it interesting.
Andrew
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ef992a35-8d35-48ff-ac1f-d0ea544ffa8an%40googlegroups.com.