Positive coverage: prove_wc / alias eq
alias eq| Line | Coverage | Source |
|---|---|---|
| 111 | ✗ | (prove_eq(decls, env, assumptions, alias_ty, ty) => c) |
| ──────── ("alias eq") | ||
| 113 | 1 | (prove_wc(decls, env, assumptions, Predicate::AliasEq(alias_ty, ty)) => c) |
1 test exercised this rule:
Source location: tests/projection.rs:115
#[test]
fn projection_equality() {
test_where_clause(
PROJECTION_EQUALITY,
"exists<U> {} => { Trait1(S), <S as Trait1<>>::Type = U }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => <S as Trait1>::Type} }}"]);
test_where_clause(PROJECTION_EQUALITY, "exists<U> {} => { Trait2(S, U) }")
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => <S as Trait1>::Type} }}"]);
}
Proof tree
prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_eq (symmetric)prove_eq.rs:41prove_eq (existential)prove_eq.rs:65prove_existential_var_eq (existential-nonvar)prove_eq.rs:98prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_eq (existential)prove_eq.rs:65prove_existential_var_eq (existential-existential)prove_eq.rs:123
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (some)prove_wc_list.rs:31prove_wc (alias eq)prove_wc.rs:112prove_eq (normalize-l)prove_eq.rs:72prove_normalize (normalize-via-impl)prove_normalize.rs:49prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_eq (symmetric)prove_eq.rs:41prove_eq (existential)prove_eq.rs:65prove_existential_var_eq (existential-nonvar)prove_eq.rs:98prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_eq (symmetric)prove_eq.rs:41prove_eq (existential)prove_eq.rs:65prove_existential_var_eq (existential-nonvar)prove_eq.rs:98prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_eq (existential)prove_eq.rs:65prove_existential_var_eq (existential-existential)prove_eq.rs:123
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (some)prove_wc_list.rs:31prove_wc (alias eq)prove_wc.rs:112prove_eq (symmetric)prove_eq.rs:41prove_eq (existential)prove_eq.rs:65prove_existential_var_eq (existential-nonvar)prove_eq.rs:98prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24