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: prove_normalize_via / axiom-r

axiom-r
LineCoverageSource
102✗(if let None = goal.downcast::<ExistentialVar>())
103✗(if goal != b)
104✗(prove_syntactically_eq(decls, env, assumptions, a, goal) => c)
105N/A(let b = c.substitution().apply(b))
──────── ("axiom-r")
1071(prove_normalize_via(decls, env, assumptions, Predicate::Equals(b, a), goal) => Constrained(b, c))

1 test exercised this rule:

Source location: tests/coherence_overlap.rs:237 (all coverage from this test)

#[test]
fn neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
    FormalityTest::new(crates![crate core {
        #![feature(negative_impls)]
        trait CoreTrait {}
        struct CoreStruct {}
        impl !CoreTrait for CoreStruct {}
    },
    crate foo {
        trait FooTrait {}
        impl<T> FooTrait for T where T: CoreTrait {}
        impl FooTrait for CoreStruct {}
    }])
    .skip_execute()
    .ok()
}
Proof tree