Negative coverage: prove_eq / rigid / premise prove(decls, env, assumptions, Predicates::all_eq(a_parameters, b_parameters)) => c
Premise at line 47. Observed failure causes: failed_judgment.
rigid| Line | Coverage | Source |
|---|---|---|
| 44 | N/A | (let RigidTy { name: a_name, parameters: a_parameters } = a) |
| 45 | N/A | (let RigidTy { name: b_name, parameters: b_parameters } = b) |
| 46 | ✗ | (if a_name == b_name) |
| 47 | 1 | (prove(decls, env, assumptions, Predicates::all_eq(a_parameters, b_parameters)) => c) |
| ──────── ("rigid") | ||
| 49 | 201 | (prove_eq(decls, env, assumptions, Ty::RigidTy(a), Ty::RigidTy(b)) => c) |
1 test failed proving this premise:
Source location: tests/drop.rs:274 (all coverage from this test)
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "trait impl"mod.rs:195check_drop_impl_always_applicable failedimpls.rs:330rule "Drop impl is always applicable"impls.rs:360prove failedfunction.rs:250args
rulefunction.rs:250prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "positive impl"prove_predicate.rs:71prove failedprove_predicate.rs:71args
ruleprove_predicate.rs:71prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "rigid"prove_eq.rs:47prove failedprove_eq.rs:47args
ruleprove_eq.rs:47prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "rigid"prove_eq.rs:47prove failedprove_eq.rs:47args
ruleprove_eq.rs:47prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args