We need to see if we can make the explanation we will give
to end users is understandable.
I'll make an attempt.
@ can be used in two contexts:
1. When used without the {}, it means HEAD.
2. When used with a {}, it means what those three forms individually
mean. @{} already implies HEAD: don't put an extra @.
I think it's the cleanest.