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 / scalar constants are always wf

scalar constants are always wf
LineCoverageSource
──────── ("scalar constants are always wf")
793(prove_wf(_decls, env, _assumptions, ConstData::Scalar(_)) => Constraints::none(env))

3 tests exercised this rule:


Source location: tests/consts.rs:11

#[test]
fn nonsense_rigid_const_bound() {
    FormalityTest::new(crates![crate Foo {
        // This where-clause is not *provable*, but it is well-formed.
        trait Foo where type_of_const true is u32 {}
    }])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 983 nodes shown)

Source location: tests/consts.rs:58

#[test]
fn rigid_const_bound() {
    FormalityTest::new(crates![crate Foo {
        trait Foo where type_of_const true is bool {}
    }])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 983 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)