These names are only visible under "ensures" but not under "returns".
If the result is named, the special variable "result" is not used.
In a tuple, either each component should be named, or none at all.
Underscores are allowed. Parentheses around the return type are required.
Each name must be given its own type: "f () : (x y: int)" is rejected.
Identifiers without cast are treated as types, not as names.
To name the result without giving its type, use "returns".
