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 orphan_check

judgment_fn! {
    fn orphan_check(program: Program, impl_a: TraitImpl) => () {
        /* rules omitted */
    }
}

Source: crates/formality-rust/src/check/coherence.rs:30

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.

orphan_check
LineCoverageSource
35✗(scope(enter_universally(Env::default(), &impl_a.binder) => (env, a)) with()
(let trait_ref = a.trait_ref())
(prove_goal(program, env, &a.where_clauses, AtomicPredicate::is_local(trait_ref)) => ()))
──────── ("orphan_check")
39210(orphan_check(program, impl_a) => ())

How to read this page