Negative coverage: check_trait_impl_item / fn in impl / premise check_fn_in_impl(program, env, assumptions, trait_items, v, crate_id) => ()

Premise at line 163. Observed failure causes: failed_judgment.

3 tests failed proving this premise:

Source location: tests/drop.rs:83 (all coverage from this test)

Source location: tests/drop.rs:192 (all coverage from this test)

fn drop<'a>(self: &'a MyStruct) -> () {}
}
}])
rr(expect_test::expect![[r#"
r[E0053]: method `drop` has an incompatible type for trait
 lib.rs
|
    fn drop<'a10>(mut self: &'a10 MyStruct) -> () {}
                            ^^^^^^^^^^^^^^ types differ in mutability
|
note: expected signature `fn(&mut MyStruct)`
         found signature `fn(&MyStruct)`
: change the self-receiver type to match the trait
|
    fn drop<'a10>(mut self: &'a10 MyStruct) -> () {}
    fn drop<'a10>(mut &mut self) -> () {}
|

more information about this error, try `rustc --explain E0053`.
r: could not compile `Foo` (lib) due to 1 previous error
"#]])
ect_test::expect![[r#"
es/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: &!lt_0 mut MyStruct, assumptions: {}, env: Env { variables: [!lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

es/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: &!lt_0 MyStruct, assumptions: {}, env: Env { variables: [!lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}

ust return unit, even when its body matches another return type.
#[test]
_non_unit_return() {
yTest::new(crates![crate Foo {
ct MyStruct {}

 Drop for MyStruct {
fn drop<'a>(self: &'a mut MyStruct) -> u32 {
    return 0_u32;
}

Source location: tests/drop.rs:228 (all coverage from this test)

fn drop<'a>(self: &'a mut MyStruct) -> u32 {
    return 0_u32;
}

How to read this page