Macro contracts_requires

Attribute macro applied to a function to give it a precondition.

The attribute carries an argument token-tree which is eventually parsed as an boolean expression with access to the function's formal parameters