On Wed, 22 Sept 2021 at 22:41, Gašper Ažman via Liaison
<liaison_at_[hidden]> wrote:
> post(audit, new) [r=return, x, y] { // seems like lambda-like captures fit in
> {r % x == 0};
> {r % y == 0};
> }

Intriguing. This approach allows me to write postconditions for
parameters that aren't const.
The capture allows me to decide whether to capture the original value
or a reference to a possibly
changing value, and it allows me to perform init-capture shenanigans
to capture whichever transformation
of a move-only type, too, or a transformation of a non-deep-const type, too.