Judgment check_drop_impl_always_applicable
judgment_fn! {
/// Check that a `Drop` impl is "always applicable": for any instance of the ADT
/// (with its where-clauses satisfied), the Drop impl must apply.
pub(super) fn check_drop_impl_always_applicable(
program: Program,
trait_impl: TraitImpl,
crate_id: CrateId,
) => () {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/impls.rs:330
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 |
|---|---|---|
| 341 | ✗ | (if **trait_impl.trait_id() != *"Drop") |
| ──────── ("not a Drop impl") | ||
| 343 | 210 | (check_drop_impl_always_applicable(program, trait_impl, crate_id) => ()) |
Drop impl is always applicable| Line | Coverage | Source |
|---|---|---|
| 347 | ✗ | (if **trait_impl.trait_id() == *"Drop") |
| 349 | 1 | (let adt_id = drop_impl_adt_id(&trait_impl)?) |
| 351 | 1 | (check_drop_impl_in_defining_crate(program, adt_id, crate_id) => ()) |
| 352 | ✗ | (let adt = program.program().adt_item_named(adt_id)?.to_adt()) |
| 354 | ✗ | (scope(enter_universally(Env::default(), &with_variables(&adt.binder)) => (env, (adt_parameters, AdtBoundData { where_clauses, variants: _ }))) with() (let adt_self_ty = Ty::rigid(adt_id, adt_parameters)) // Prove: under the ADT's where-clauses, Drop is implemented for the ADT. // This will find the impl, unify its self type, and verify its where-clauses. (let drop_trait_ref = crate::grammar::TraitId::new("Drop").with(adt_self_ty, ())) (super::prove_goal(program, env, where_clauses, AtomicPredicate::is_implemented(drop_trait_ref)) => ())) |
| ──────── ("Drop impl is always applicable") | ||
| 363 | 5 | (check_drop_impl_always_applicable(program, trait_impl, crate_id) => ()) |