Judgment check_drop_impl_always_applicable at crates/formality-rust/src/check/impls.rs:328
Signature:
check_drop_impl_always_applicable(program: Program, trait_impl: TraitImpl, crate_id: CrateId,) => ()The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.
not a Drop impl| Line | Coverage | Source |
|---|---|---|
| 339 | ✗ | (if **trait_impl.trait_id() != *"Drop") |
| ──────── ("not a Drop impl") | ||
| 341 | 127 | (check_drop_impl_always_applicable(program, trait_impl, crate_id) => ()) |
Drop impl is always applicable| Line | Coverage | Source |
|---|---|---|
| 345 | ✗ | (if **trait_impl.trait_id() == *"Drop") |
| 347 | 1 | (let adt_id = drop_impl_adt_id(&trait_impl)?) |
| 349 | 1 | (check_drop_impl_in_defining_crate(program, adt_id, crate_id) => ()) |
| 350 | ✗ | (let adt = program.program().adt_item_named(adt_id)?.to_adt()) |
| 352 | N/A | (let (env, adt_vars) = Env::default().universal_substitution(&adt.binder)) |
| 353 | ✗ | (let adt_bound = adt.binder.instantiate_with(adt_vars)?) |
| 354 | N/A | (let adt_self_ty = Ty::rigid(adt_id, adt_vars)) |
| 357 | N/A | (let drop_trait_ref = crate::grammar::TraitId::new("Drop").with(adt_self_ty, ())) |
| 358 | 3 | (super::prove_goal(&program, &env, &adt_bound.where_clauses, Predicate::IsImplemented(drop_trait_ref.clone())) => ()) |
| ──────── ("Drop impl is always applicable") | ||
| 361 | 6 | (check_drop_impl_always_applicable(program, trait_impl, crate_id) => ()) |