Macro contracts_ensures

Attribute macro applied to a function to give it a post-condition.

The attribute carries an argument token-tree which is eventually parsed as a unary closure expression that is invoked on a reference to the return value.