# Hillel Wayne - Labels :: Learn TLA+ (Highlights)  ## Highlights - The first line in a process has to have a label. - A label must come before a `while` statement. - A label must come right after a `call`, `return`, or `goto`. - If you have a control statement, such as `if` or `either`, and one possible branch has a label in it, then the whole control structure must be followed with a label. - You cannot put labels in a `with` statement. - You cannot assign to any given variable more than once in a label. - switching two variables, or assigning to different records of the same structure. In these cases you can use `||` to chain assignments