Xavier Denis

I've proved that an identity map and incrementing map are safe but have not yet checked their results (i'm scared of looking at the proofs).

@jhjourdan I'm going to merge `Map` despite not having working benchmarks. We can fine tune the spec of `map` afterwards.

I'm having a hard time recreating this issue at the moment...

A quick inspection appears to show that the issue is that associated types are improperly normalized for inherited specifications. This can be confirmed by removing https://github.com/xldenis/creusot/blob/master/creusot-contracts/src/std/slice.rs#L336-L356 and looking at the...

I think I have a potential solution to this and thus #616. In `before_analysis` we can request the `mir_promoted` for every `const fn` in the crate. We can put it...

> This appears to have fixed things for me. I can't reproduce the errors described in https://github.com/xldenis/creusot/issues/616 any more. Wait, what? I haven't performed this proposed change, is this something...

I believe this is fixed since we now always export `Model` in `creusot-contracts`.

From @dewert99 ``` enum Bad

I'm going to close this as wont-fix as there is no real roadmap for this being added (nor a usecase).

I think this is pretty trivial to check in a lint :)