option: rm implementation of Add

Closes #6002

There is consensus that the current definition is the wrong choice.
It's not clear whether this is worth including, but for now it can be
removed.