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

const has ty
LineCoverageSource
1551(prove_const_has_type(decls, env, assumptions, constant) => (ty_constant, c))
1561(prove_after(decls, c, assumptions, AtomicPredicate::equals(ty_constant, ty)) => c)
──────── ("const has ty")
1584(prove_predicate(decls, env, assumptions, AtomicPredicate::ConstHasType(constant, ty)) => c)

4 tests exercised this rule:

Source location: tests/const_generics_rv_tsv_parse.rs:12 (all coverage from this test)

#[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()
    .rustc_ok()
    .ok()
}
Proof tree
… (200 of 3485 nodes shown)

Source location: tests/consts.rs:53 (all coverage from this test)

#[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 3485 nodes shown)

Source location: tests/consts.rs:166 (all coverage from this test)

Proof tree
… (200 of 3574 nodes shown)

Source location: tests/well_formed_trait_ref.rs:86 (all coverage from this test)

#[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 3515 nodes shown)

How to read this page