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: orphan_check_neg / orphan_check_neg

orphan_check_neg
LineCoverageSource
56N/A(let (env, a) = Env::default().instantiate_universally(&impl_a.binder))
57N/A(let trait_ref = a.trait_ref())
581(prove_goal(program, env, &a.where_clauses, Predicate::is_local(trait_ref)) => ())
──────── ("orphan_check_neg")
603(orphan_check_neg(program, impl_a) => ())

3 tests exercised this rule:


Source location: tests/basic_tests.rs:179

#[test]
fn non_lifetime_binder_in_neg_trait_impl_where_clause_pass() {
    FormalityTest::new(crates![crate core {
        #![feature(non_lifetime_binders)]
        trait A<T> where T: B { }

        trait B { }

        impl<T> !A<T> for u32 where for<U> u32: A<U> { }

        impl <T> B for T {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/coherence_overlap.rs:147

#[test]
fn neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
    FormalityTest::new(crates![crate core {
        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

Source location: tests/decl_safety.rs:32

#[test]
fn unsafe_trait_negative_impl() {
    FormalityTest::new(crates![crate baguette {
        unsafe trait Foo {}
        impl !Foo for u32 {}
    }])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 997 nodes shown)