marking an operator 'deprecated' leads to error messages with strings like "$plus"