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: check_drop_impl_always_applicable / Drop impl is always applicable

Drop impl is always applicable
LineCoverageSource
300✗(if **trait_impl.trait_id() == *"Drop")
3021(let adt_id = drop_impl_adt_id(&trait_impl)?)
303✗(let adt = program.program().adt_item_named(adt_id)?.to_adt())
305N/A(let (env, adt_vars) = Env::default().universal_substitution(&adt.binder))
306✗(let adt_bound = adt.binder.instantiate_with(adt_vars)?)
307N/A(let adt_self_ty = Ty::rigid(adt_id, adt_vars))
310N/A(let drop_trait_ref = crate::grammar::TraitId::new("Drop").with(adt_self_ty, ()))
3112(super::prove_goal(&program, &env, &adt_bound.where_clauses,
Predicate::IsImplemented(drop_trait_ref.clone())) => ())
──────── ("Drop impl is always applicable")
3144(check_drop_impl_always_applicable(program, trait_impl) => ())

4 tests exercised this rule:

Source location: tests/drop.rs:20

#[test]
fn drop_impl_simple_struct() {
    FormalityTest::new(crates![
        crate Foo {
            struct MyStruct {
                value: u32,
            }

            impl Drop for MyStruct {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1058 nodes shown)

Source location: tests/drop.rs:38

#[test]
fn drop_impl_generic_struct() {
    FormalityTest::new(crates![
        crate Foo {
            trait Clone {}

            struct MyStruct<T> where T: Clone {
                value: T,
            }

            impl<T> Drop for MyStruct<T> where T: Clone {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1108 nodes shown)

Source location: tests/drop.rs:54

#[test]
fn drop_impl_generic_no_where_clauses() {
    FormalityTest::new(crates![
        crate Foo {
            struct Wrapper<T> {
                value: T,
            }

            impl<T> Drop for Wrapper<T> {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1074 nodes shown)

Source location: tests/drop.rs:78

#[test]
fn drop_impl_subset_where_clauses() {
    FormalityTest::new(crates![
        crate Foo {
            trait Clone {}
            trait Debug {}

            struct MyStruct<T> where T: Clone, T: Debug {
                value: T,
            }

            // Impl has no where-clauses — but the struct requires them.
            impl<T> Drop for MyStruct<T> {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1096 nodes shown)