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_wc / const has ty

const has ty
LineCoverageSource
1651(prove_const_has_type(decls, env, assumptions, constant) => (ty_constant, c))
1661(prove_after(decls, c, assumptions, Relation::equals(ty_constant, ty)) => c)
──────── ("const has ty")
1683(prove_wc(decls, env, assumptions, Predicate::ConstHasType(constant, ty)) => c)

3 tests exercised this rule:

Source location: tests/const_generics_rv_tsv_parse.rs:11

#[test]
fn parse_minirust_22() {
    FormalityTest::new(crates![crate Foo {
        trait Trait<const N> where type_of_const N is usize {}
        impl Trait<usize(22)> for u32 {}
    }])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1056 nodes shown)

Source location: tests/consts.rs:49

#[test]
fn holds() {
    FormalityTest::new(crates![crate Foo {
        trait Foo<const C> where type_of_const C is bool {}

        impl Foo<true> for u32 {}
    }])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1056 nodes shown)

Source location: tests/well_formed_trait_ref.rs:86

#[test]
fn const_param() {
    FormalityTest::new(crates![crate foo {
        trait Trait1<const C> where type_of_const C is u32 {}

        struct S1 {}

        impl Trait1<u32(3)> for S1 {}

        struct S2 where S1: Trait1<u32(3)> {}
    }])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1084 nodes shown)