Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Positive coverage: overlap_check_impl / inverted

inverted
LineCoverageSource
114✗(if impl_a != impl_b)
115✗(if impl_a.trait_id() == impl_b.trait_id())
116N/A(let (env, a) = Env::default().instantiate_universally(&impl_a.binder))
117N/A(let (env, b) = env.instantiate_universally(&impl_b.binder))
1181(wc in a.where_clauses.iter().chain(&b.where_clauses).flat_map(|wc| wc.invert()))
1195(prove_goal(program, env, (Wcs::all_eq(&a.trait_ref().parameters, &b.trait_ref().parameters), &a.where_clauses, &b.where_clauses), wc) => ())
──────── ("inverted")
1211(overlap_check_impl(program, impl_a, impl_b) => ())

1 test exercised this rule:

Source location: tests/coherence_overlap.rs:237 (all coverage from this test)

#[test]
fn neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
    FormalityTest::new(crates![crate core {
        #![feature(negative_impls)]
        trait CoreTrait {}
        struct CoreStruct {}
        impl !CoreTrait for CoreStruct {}
    },
    crate foo {
        trait FooTrait {}
        impl<T> FooTrait for T where T: CoreTrait {}
        impl FooTrait for CoreStruct {}
    }])
    .skip_execute()
    .ok()
}
Proof tree