Postconditions specified more than once always cause compile error

[PeterBindels-TomTom]

int f() post(r: r > 0);
int f() post(r: r > 0);

or even

#define F(X) X; X
F(int f() post(r: r > 0));

the compiler claims

<source>:7:5: error: function redeclaration differs in contract specifier sequence
    7 | int f() post(r: r > 0);
      |     ^   ~~~~~~~~~~~~~
<source>:7:9: note: in contract specified here
    7 | int f() post(r: r > 0);
      |         ^       ~~~~~
<source>:6:9: note: contract previously specified with a non-equivalent condition
    6 | int f() post(r: r > 0);
      |         ^       ~~~~~```

Contracts may be redeclared according to P2900 if they specify the same contract (https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p2900r8.pdf page 68, quote "A declaration E of a function f that is not a first declaration shall have either no function-contract-specifier-seq or the same function-contract-specifier-seq as any first declaration D reachable from E.")

[EricWF]

Yeah, so the bug here is that the compiler is seeing two different declarations of r and then assuming they're not equivalent because they're not the exact same declaration.

The fix is to compare them like parameters, which means checking the type and the function scope depth to establish equality. Fix incoming shortly.

[EricWF]

A partial fix is in 00aafdc5d7d23ad7f77271453eaa66dd341d2e1b,

~I think this current fix will accept things like that below~

I think the below code is always invalid because you can't re declare a contract containing a lambda?

int f() post(r :  []() post(s : s > 0) { return r; }());
int f() post(r : []() post(s : r > 0) { return r; }()); 

[PeterBindels-TomTom]

Yep, those lambdas are by definition never the same. Those without lambdas though should be fine.