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

check_neg_trait_impl
LineCoverageSource
59N/A(let (env, bound_data) = Env::default().instantiate_universally(binder))
60N/A(let NegTraitImplBoundData { trait_id, self_ty, trait_parameters, where_clauses } = bound_data)
61N/A(let trait_ref = trait_id.with(self_ty, trait_parameters))
62(super::where_clauses::prove_where_clauses_well_formed(program, &env, &where_clauses, &where_clauses) => ())
63(super::prove_goal(program, &env, &where_clauses, Predicate::not_implemented(&trait_ref)) => ())
──────── ("check_neg_trait_impl")
653(check_neg_trait_impl(program, NegTraitImpl { binder, safety: Safety::Safe }) => ())

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)