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_impl / check_trait_impl / premise check_all_required_items_present(trait_items, impl_items) => ()

Premise at line 39. Observed failure causes: inapplicable.

check_trait_impl
LineCoverageSource
22N/A(let TraitImpl { binder, safety: _ } = &trait_impl)
23N/A(let (env, bound_data) = Env::default().instantiate_universally(binder))
24N/A(let TraitImplBoundData { trait_id, self_ty, trait_parameters, where_clauses, impl_items } = bound_data)
25N/A(let trait_ref = trait_id.with(self_ty, trait_parameters))
27✗(super::where_clauses::prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ())
282(super::prove_goal(program, env, where_clauses, Predicate::is_implemented(trait_ref)) => ())
292(super::prove_not_goal(program, env, where_clauses, Predicate::not_implemented(trait_ref)) => ())
31✗(let trait_decl = program.program().trait_named(&trait_ref.trait_id)?)
32✗(let TraitBoundData { where_clauses: _, trait_items } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?)
332(check_safety_matches(&trait_decl, &trait_impl) => ())
352(check_duplicate_impl_items(impl_items) => ())
36✗(for_all(impl_item in impl_items)
(check_trait_impl_item(program, env, where_clauses, trait_items, impl_item, crate_id) => ()))
392(check_all_required_items_present(trait_items, impl_items) => ())
──────── ("check_trait_impl")
42127(check_trait_impl(program, trait_impl, crate_id) => ())

2 tests failed proving this premise:

Source location: tests/basic_tests.rs:425 (all coverage from this test)

Failed proof tree

Source location: tests/basic_tests.rs:442 (all coverage from this test)

Failed proof tree