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

Positive coverage: is_not_downstream / via normalize

via normalize
LineCoverageSource
2621(prove_normalize(decls, env, assumptions, parameter) => Constrained(p, c1))
263N/A(let assumptions = c1.substitution().apply(assumptions))
264(is_not_downstream(decls, c1.env(), assumptions, p) => c2)
──────── ("via normalize")
2661(is_not_downstream(decls, env, assumptions, parameter) => c1.seq(c2))

1 test exercised this rule:


Source location: tests/coherence_orphan.rs:196

#[test]
fn CoreTraitLocal_for_AliasToKnown_in_Foo() {
    // TODO: see comment in `orphan_check` from prev commit
    FormalityTest::new(crates![crate core {
        trait CoreTrait<T> {}

        trait Unit {
            type Assoc : [];
        }

        impl<T> Unit for T {
            type Assoc = ();
        }
    },
    crate foo {
        struct FooStruct {}
        impl CoreTrait<FooStruct> for <() as Unit>::Assoc {}
    }])
    .skip_execute()
    .ok()
}
Proof tree