Test `holds`

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()
}

Rules proved (35)

Judgment	Rule	All tests of this rule
check_all_crates	check all prefixes	131 tests
check_associated_ty	check associated ty	116 tests
check_associated_ty_value	check_associated_ty_value	115 tests
check_coherence	check_coherence	131 tests
check_crate	check crate	131 tests
check_crate_item	trait	131 tests
check_crate_item	trait impl	127 tests
check_drop_impl_always_applicable	not a Drop impl	127 tests
check_safety_matches	safety matches	127 tests
check_trait	check trait	131 tests
check_trait_impl	check_trait_impl	127 tests
check_trait_impl_item	associated ty value	115 tests
check_trait_item	associated ty in trait	116 tests
is_local_trait_ref	local trait	126 tests
orphan_check	orphan_check	127 tests
`overlap_check`	`not_goal`	115 tests (not in the report)
`overlap_check`	`skip_different_trait`	115 tests (not in the report)
`overlap_check`	`skip_same_impl`	127 tests (not in the report)
prove_after	prove_after	154 tests
prove_const_has_type	rigid constant	3 tests
prove_eq	existential	141 tests
prove_eq	rigid	119 tests
prove_eq	symmetric	138 tests
prove_existential_var_eq	existential-universal	132 tests
`prove_outlives`	`outlive through assumption`	113 tests (not in the report)
prove_wc	const has ty	3 tests
prove_wc	eq	148 tests
prove_wc	outlives	113 tests
prove_wc	parameter well formed	121 tests
prove_wc	positive impl	136 tests
prove_wc	trait ref is local	128 tests
prove_wc_list	none	155 tests
prove_wc_list	some	154 tests
prove_wf	integers and booleans	97 tests
prove_wf	universal variables	124 tests

Premises failed (0)

This test records no negative coverage.

Proof trees

Proof tree

check_all_crates (check all prefixes) mod.rs:54
- args
- for_all mod.rs:41
  - for_all mod.rs:51
    
    args
    
    check_crate (check crate) mod.rs:75
    
    args
    
    for_all mod.rs:60
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait) mod.rs:188
    
    args
    
    check_trait (check trait) traits.rs:26
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args

… (200 of 1056 nodes shown)

Keyboard shortcuts

A MIR Formality

Test holds

Rules proved (35)

Premises failed (0)

Proof trees

Test `holds`