Signature:
overlap_check_impl(program: Program, impl_a: TraitImpl, impl_b: 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.
same impl
| Line | Coverage | Source |
|---|
| 72 | 6 | (if impl_a == impl_b) |
| | ──────── ("same impl") |
| 74 | 127 | (overlap_check_impl(_program, impl_a, impl_b) => ()) |
different trait
| Line | Coverage | Source |
|---|
| 79 | 6 | (if impl_a.trait_id() != impl_b.trait_id()) |
| | ──────── ("different trait") |
| 81 | 115 | (overlap_check_impl(_program, impl_a, impl_b) => ()) |
not goal
| Line | Coverage | Source |
|---|
| 102 | ✗ | (if impl_a != impl_b) |
| 103 | ✗ | (if impl_a.trait_id() == impl_b.trait_id()) |
| 104 | N/A | (let (env, a) = Env::default().instantiate_universally(&impl_a.binder)) |
| 105 | N/A | (let (env, b) = env.instantiate_universally(&impl_b.binder)) |
| 106 | 6 | (prove_not_goal(program, env, (), (Wcs::all_eq(&a.trait_ref().parameters, &b.trait_ref().parameters), &a.where_clauses, &b.where_clauses)) => ()) |
| | ──────── ("not goal") |
| 108 | 115 | (overlap_check_impl(program, impl_a, impl_b) => ()) |
inverted
| Line | Coverage | Source |
|---|
| 114 | ✗ | (if impl_a != impl_b) |
| 115 | ✗ | (if impl_a.trait_id() == impl_b.trait_id()) |
| 116 | N/A | (let (env, a) = Env::default().instantiate_universally(&impl_a.binder)) |
| 117 | N/A | (let (env, b) = env.instantiate_universally(&impl_b.binder)) |
| 118 | 1 | (wc in a.where_clauses.iter().chain(&b.where_clauses).flat_map(|wc| wc.invert())) |
| 119 | 5 | (prove_goal(program, env, (Wcs::all_eq(&a.trait_ref().parameters, &b.trait_ref().parameters), &a.where_clauses, &b.where_clauses), wc) => ()) |
| | ──────── ("inverted") |
| 121 | 1 | (overlap_check_impl(program, impl_a, impl_b) => ()) |