Xia Li-yao

1. I think `verif` wasn't being created because you had run `cargo creusot` previously (while upgrading your project), and then removed `verif` to clean up, and then ran `cargo creusot`...

I wonder if we can use CPS as a workaround? ``` unsafe fn with_mut_vec(&mut self, k: for R) -> R ```

I forgot TApp!

Yeah it turns out I dodged the one difficult construct.

Right now it looks online to me, but it's an http link, which may be a problem depending on browser extensions; and the https certificate is out of date.

Thanks for the report. We can probably produce an error message that explains that QuickChick commands currently can't be used in a module.

Thanks! I didn't know that. At least it works with `#[invariant(true)]`.

I'm tempted to classify this as wontfix. Maybe we can also have a list of this kind of corner cases in the documentation, so I'll leave this open to remember...

That sounds good to me. 1. Install `creusot-rustc` as `creusot-rustc-` 2. Drop the hardcoded toolchain in `cargo-creusot`, using the active toolchain instead, with a nice error message if the corresponding...

If project A uses a version of creusot built with toolchain X and project B uses another version of creusot built with toolchain Y, wouldn't you want to be able...