Xia Li-yao

Closed by #1764, which undoes #1212. In the end, the creusot-rustc options are not meant to change in regular usage, and in any case they only affect the output Coma...

Changing `filter` makes sense to me. How this commit? At the moment I'm using the browser build.

Indeed this works for me.

I'm trying to define traits that gather the necessary constraints, e.g., ``` // Extends std::PartialOrd with additional constraints for translation trait MyPartialOrd where Self: PartialOrd + DeepModel, ::DeepModelTy: OrdLogic {...

How does it do that? the only way I can think of is to somehow shadow traits from `std` but I don't see where that is happening (which is why...

OK that's good to know (including the fact that there is no consensus on `iter`). In any case, we only want to be able to refer to those names in...

Can we name it `: ViewL a ```

Do you have a minimal cargo project to reproduce this crash? I tried a simple `lib.rs` with just this `min` function and compilation succeeded. Possibly the `unwrap` should be replaced...

Minimized test case: ```rust extern crate creusot_contracts; use creusot_contracts::{*, PartialEq}; #[derive( PartialEq, DeepModel, )] pub struct BaseCurrency(pub Decimal) where I: Sized; #[derive( PartialEq, // DeepModel, )] pub struct Decimal(pub I);...

The crash goes away if I compile the `./expand`-ed code. :)