Judgment overlap_check_impl
judgment_fn! {
/// Holds if `impl_a` and `impl_b` cannot apply to the same types.
/// Trivially holds for the same impl or for impls of different traits.
fn overlap_check_impl(program: Program, impl_a: TraitImpl, impl_b: TraitImpl) => () {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/coherence.rs:64
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 | 9 | (if impl_a == impl_b) |
| ──────── ("same impl") | ||
| 74 | 210 | (overlap_check_impl(_program, impl_a, impl_b) => ()) |
different trait| Line | Coverage | Source |
|---|---|---|
| 79 | 9 | (if impl_a.trait_id() != impl_b.trait_id()) |
| ──────── ("different trait") | ||
| 81 | 194 | (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 | ✗ | (scope(enter_universally(Env::default(), &impl_a.binder) => (env, a)) with() (scope(enter_universally(env, &impl_b.binder) => (env, b)) with() (prove_not_goal(program, env, (), (Predicates::all_eq(&a.trait_ref().parameters, &b.trait_ref().parameters), &a.where_clauses, &b.where_clauses)) => ()))) |
| ──────── ("not goal") | ||
| 108 | 195 | (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 | ✗ | (scope(enter_universally(Env::default(), &impl_a.binder) => (env, a)) with() (scope(enter_universally(env, &impl_b.binder) => (env, b)) with() (wc in a.where_clauses.iter().chain(&b.where_clauses).flat_map(|wc| wc.invert())) (prove_goal(program, env, (Predicates::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) => ()) |