Armaël Guéneau
Armaël Guéneau
Ah, the `#[ensures(true)]` seems to be required for the error to appear.
Thanks for the answer! I'm glad that the Teams functionality exists, and it indeed seems useful for some of the file sharing scenarios I have encountered. However, I think shared...
I had assumed that adding contracts to a logical function simply generate a proof obligation of the form `forall x y z. pre(x,y,z) ==> post(x,y,z,func(x,y,z))`, which doesn't seem to require...
> In this case, if PtrOwn itself contains a Box and not a T, the bound can be relaxed to T: ?Sized. OK, that's a good trick indeed. > Why...
(Any workaround that would allow our development to compile with Coq 8.20 is welcome, we really have no idea of what is going on...)
No not really, we just sticked to 8.19 for now.
I still don't understand. According to the changelog the syntax should be of the form `#![trigger e1,..,en]`, which means, I assume, `#![trigger e]` if there is only one trigger expression....
`#![trigger x + 1 - 1]` produces the same error (and seems difficult to parse unambiguously in more complex cases).
Likely fixed by #1592 .
I suggest we focus in this issue on why3find (the binary builds can be a separate issue) :). In the meeting this morning we discussed the following approach for testing/adopting...