There hardly can be any issues with that, but just for the sake of having the code exactly reflected to TLA+ lets do it anyway.