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())
116✗(scope(enter_universally(Env::default(), &impl_a.binder) => (env, a)) with()
(scope(enter_universally(env, &impl_b.binder) => (env, b)) with()
(wc in a.where_clauses.iter().chain(&b.where_clauses).flat_map(|wc| wc.invert()))
(prove_goal(program, env, (Predicates::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

How to read this page