Judgment check_drop_impl_always_applicable at crates/formality-rust/src/check/impls.rs:284
Signature:
check_drop_impl_always_applicable(program: Program, trait_impl: TraitImpl,) => ()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 |
|---|---|---|
| 294 | ✗ | (if **trait_impl.trait_id() != *"Drop") |
| ──────── ("not a Drop impl") | ||
| 296 | 110 | (check_drop_impl_always_applicable(program, trait_impl) => ()) |
Drop impl is always applicable| Line | Coverage | Source |
|---|---|---|
| 300 | ✗ | (if **trait_impl.trait_id() == *"Drop") |
| 302 | 1 | (let adt_id = drop_impl_adt_id(&trait_impl)?) |
| 303 | ✗ | (let adt = program.program().adt_item_named(adt_id)?.to_adt()) |
| 305 | N/A | (let (env, adt_vars) = Env::default().universal_substitution(&adt.binder)) |
| 306 | ✗ | (let adt_bound = adt.binder.instantiate_with(adt_vars)?) |
| 307 | N/A | (let adt_self_ty = Ty::rigid(adt_id, adt_vars)) |
| 310 | N/A | (let drop_trait_ref = crate::grammar::TraitId::new("Drop").with(adt_self_ty, ())) |
| 311 | 2 | (super::prove_goal(&program, &env, &adt_bound.where_clauses, Predicate::IsImplemented(drop_trait_ref.clone())) => ()) |
| ──────── ("Drop impl is always applicable") | ||
| 314 | 4 | (check_drop_impl_always_applicable(program, trait_impl) => ()) |