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_const_has_type / rigid constant

rigid constant
LineCoverageSource
──────── ("rigid constant")
293(prove_const_has_type(_decls, env, _assumptions, ConstData::Scalar(scalar)) => (scalar.ty(), Constraints::none(env)))

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)