Full name of submitter (unless configured in github; will be published with the issue): Yin Xinyu
[dcl.contract.res]/1 says
The result-name-introducer of a postcondition-specifier is a declaration. The result-name-introducer introduces the identifier as the name of a result binding of the associated function....
However, it betrays [basic.pre] bullet (5.4)
Every name is introduced by a declaration, which is a
Suggested resolution:
Either edit [dcl.contract.res]/1
The result-name-introducer of a postcondition-specifier is a declaration. The result-name-introducer introduces the identifier as the name of a result binding of the associated function....
or edit [basic.pre] bullet (5.4)
identifier in a result-name-introducer in a postcondition assertion ([dcl.contract.res]),
Full name of submitter (unless configured in github; will be published with the issue): Yin Xinyu
[dcl.contract.res]/1 says
However, it betrays [basic.pre] bullet (5.4)
Suggested resolution:
Either edit [dcl.contract.res]/1
or edit [basic.pre] bullet (5.4)