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

Judgment check_trait_impl

judgment_fn! {
    pub(super) fn check_trait_impl(
        program: Program,
        trait_impl: TraitImpl,
        crate_id: CrateId,
    ) => () {
        /* rules omitted */
    }
}

Source: crates/formality-rust/src/check/impls.rs:14

The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.

check_trait_impl
LineCoverageSource
22N/A(let TraitImpl { binder, safety: _ } = &trait_impl)
23✗(scope(enter_universally(Env::default(), binder) => (env, TraitImplBoundData { trait_id, self_ty, trait_parameters, where_clauses, impl_items })) with()
(let trait_ref = trait_id.with(self_ty, trait_parameters))

(super::where_clauses::prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ())
(super::prove_goal(program, env, where_clauses, AtomicPredicate::is_implemented(trait_ref)) => ())
(super::prove_not_goal(program, env, where_clauses, AtomicPredicate::not_implemented(trait_ref)) => ())

(let trait_decl = program.program().trait_named(&trait_ref.trait_id)?)
(let TraitBoundData { where_clauses: _, trait_items } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?)
(check_safety_matches(&trait_decl, &trait_impl) => ())

(check_duplicate_impl_items(impl_items) => ())
(for_all(impl_item in impl_items)
(check_trait_impl_item(program, env, where_clauses, trait_items, impl_item, crate_id) => ()))

(check_all_required_items_present(trait_items, impl_items) => ()))
──────── ("check_trait_impl")
41210(check_trait_impl(program, trait_impl, crate_id) => ())

How to read this page