One would write x = a -> b to make x change its value from a to b. This is syntactic sugar for:
precondition( x == a )
x = b
This pattern comes up a lot when you want to increase your confidence that your code is doing what you think it should be doing.