Test `u32_T_where_T_Not_impls`

Source location: tests/coherence_overlap.rs:207

#[test]
fn u32_T_where_T_Not_impls() {
    FormalityTest::new(crates![crate core {
        trait Foo {}
        impl Foo for u32 {}
        impl<T> Foo for T where T: Not {}

        trait Not {}
    }])
    .skip_execute()
    .ok()
}

Rules proved (26)

Judgment	Rule	All tests of this rule
check_all_crates	check all prefixes	131 tests
check_coherence	check_coherence	131 tests
check_crate	check crate	131 tests
check_crate_item	trait	131 tests
check_crate_item	trait impl	127 tests
check_drop_impl_always_applicable	not a Drop impl	127 tests
check_safety_matches	safety matches	127 tests
check_trait	check trait	131 tests
check_trait_impl	check_trait_impl	127 tests
is_local_trait_ref	local trait	126 tests
orphan_check	orphan_check	127 tests
`overlap_check`	`not_goal`	115 tests (not in the report)
`overlap_check`	`skip_same_impl`	127 tests (not in the report)
prove_after	prove_after	154 tests
prove_eq	existential	141 tests
prove_eq	symmetric	138 tests
prove_existential_var_eq	existential-universal	132 tests
prove_via	predicate-congruence-axiom	13 tests
prove_wc	assumption	19 tests
prove_wc	eq	148 tests
prove_wc	positive impl	136 tests
prove_wc	trait ref is local	128 tests
prove_wc	trait well formed	19 tests
prove_wc_list	none	155 tests
prove_wc_list	some	154 tests
prove_wf	universal variables	124 tests

Premises failed (0)

This test records no negative coverage.

Proof trees

Proof tree

check_all_crates (check all prefixes) mod.rs:54
- args
- for_all mod.rs:41
  - for_all mod.rs:51
    
    args
    
    check_crate (check crate) mod.rs:75
    
    args
    
    for_all mod.rs:60
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait) mod.rs:188
    
    args
    
    check_trait (check trait) traits.rs:26
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (trait well formed) prove_wc.rs:135
    
    args
    
    for_all combinators.rs:69
    
    prove_wf (universal variables) prove_wf.rs:27
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_eq (symmetric) prove_eq.rs:39
    
    args
    
    prove_eq (existential) prove_eq.rs:63
    
    args
    
    prove_existential_var_eq (existential-universal) prove_eq.rs:141
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (assumption) prove_wc.rs:49
    
    args
    
    prove_via (predicate-congruence-axiom) prove_via.rs:32
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait) mod.rs:188
    
    args
    
    check_trait (check trait) traits.rs:26
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_coherence (check_coherence) coherence.rs:24
    
    args
    
    for_all coherence.rs:8
    
    for_all coherence.rs:17
    
    args
    
    for_all coherence.rs:8
    
    for_all coherence.rs:18
    
    args
    
    overlap_check (skip_same_impl) coherence.rs:75
    
    for_all coherence.rs:18
    
    args
    
    overlap_check (not_goal) coherence.rs:135
    
    for_all coherence.rs:17
    
    args
    
    for_all coherence.rs:8
    
    for_all coherence.rs:18
    
    args
    
    overlap_check (not_goal) coherence.rs:135
    
    for_all coherence.rs:18
    
    args
    
    overlap_check (skip_same_impl) coherence.rs:75
    
    for_all coherence.rs:8
    
    for_all coherence.rs:20
    
    args
    
    orphan_check (orphan_check) coherence.rs:39
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (trait ref is local) prove_wc.rs:141
    
    args
    
    is_local_trait_ref (local trait) is_local.rs:208
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    for_all coherence.rs:20
    
    args
    
    orphan_check (orphan_check) coherence.rs:39
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (trait ref is local) prove_wc.rs:141
    
    args
    
    is_local_trait_ref (local trait) is_local.rs:208
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args

Keyboard shortcuts

A MIR Formality

Test u32_T_where_T_Not_impls

Rules proved (26)

Premises failed (0)

Proof trees

Test `u32_T_where_T_Not_impls`