[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Bug or quirk for how TLC interprets EXCEPT?

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.


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.