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

Negative coverage: check_trait / check trait / premise check_trait_items_have_unique_names(&trait_items) => ()

Premise at line 22. Observed failure causes: inapplicable.

check trait
LineCoverageSource
19N/A(let Trait { safety: _, id: _, binder } = t)
20N/A(let (env, bound_data) = env.instantiate_universally(&binder.explicit_binder))
21N/A(let TraitBoundData { where_clauses, trait_items } = bound_data)
222(check_trait_items_have_unique_names(&trait_items) => ())
232(super::where_clauses::prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ())
24(for_all(trait_item in trait_items)
(check_trait_item(program, env, where_clauses, trait_item, crate_id) => ()))
──────── ("check trait")
27114(check_trait(program, env, t, crate_id) => ())

2 tests failed proving this premise:


Source location: tests/basic_tests.rs:303

Failed proof tree

Source location: tests/basic_tests.rs:316

#[test]
fn trait_items_with_duplicate_associated_type_names() {
    FormalityTest::new(crates![crate core {
        trait A {
            type Assoc : [];
            type Assoc : [];
        }
    }])
    .err(expect_test::expect![[r#"
            the rule "check trait" at (traits.rs) failed because
              the associated type name `Assoc` is defined multiple times"#]]);
}
Failed proof tree