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_wf / aliases

aliases
LineCoverageSource
80✗(prove_alias_wf(decls, env, assumptions, name, parameters) => c)
──────── ("aliases")
825(prove_wf(decls, env, assumptions, AliasTy { name, parameters }) => c)

5 tests exercised this rule:

Source location: tests/codegen.rs:628 (all coverage from this test)

fn main() -> () {
    println!(identity::<S>(7_u32));
}
Proof tree
… (200 of 3615 nodes shown)

Source location: tests/codegen.rs:721 (all coverage from this test)

fn main() -> () {
    let w: Wrap<<S as Value>::Item> = Wrap::<<S as Value>::Item> { value: 7_u32 };
    println!(w.value);
}
Proof tree
… (200 of 3588 nodes shown)

Source location: tests/codegen.rs:798 (all coverage from this test)

fn main() -> () {
    let x: <S as Outer>::Item = 7_u32;
    println!(x);
}
Proof tree
… (200 of 3700 nodes shown)

Source location: tests/codegen.rs:927 (all coverage from this test)

fn main() -> () {
    println!(identity::<Number>(7_u32));
    println!(identity::<Flag>(true));
    println!(identity::<Number>(9_u32));
}
Proof tree
… (200 of 3845 nodes shown)

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

#[test]
fn is_local_unknowable_trait_ref() {
    FormalityTest::new(crates![crate core {
        trait Project {
            type Assoc: [];
        }

        impl<T> Project for T {
            type Assoc = T;
        }

        trait Foo<U> { }
    },
    crate foo {
        struct LocalType {}

        trait Overlap<U> {}
        impl<T, U> Overlap<U> for T
        where
            <T as Project>::Assoc: Foo<U> {}
        impl<T> Overlap<LocalType> for () {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

How to read this page