Positive coverage: prove_syntactically_eq / alias
alias| Line | Coverage | Source |
|---|---|---|
| 161 | N/A | (let AliasTy { name: a_name, parameters: a_parameters } = a) |
| 162 | N/A | (let AliasTy { name: b_name, parameters: b_parameters } = b) |
| 163 | ✗ | (if a_name == b_name) |
| 164 | 1 | (zip(decls, env, assumptions, a_parameters.clone(), b_parameters.clone(), &prove_syntactically_eq) => c) |
| ──────── ("alias") | ||
| 166 | 1 | (prove_syntactically_eq(decls, env, assumptions, TyData::AliasTy(a), TyData::AliasTy(b)) => c) |
1 test exercised this rule:
Source location: crates/formality-rust/src/prove/prove/test/eq_assumptions.rs:126
#[test]
fn test_normalize_assoc_ty_existential1() {
test_prove(
Program::empty(),
term(
"\
forall<T> \
exists<A> \
{ <T as Iterator>::Item = u32 } => { <A as Iterator>::Item = u32 }",
),
)
.assert_ok(expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }}"]);
}Proof tree
prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_eq (normalize-l)prove_eq.rs:72prove_normalize (normalize-via-assumption)prove_normalize.rs:34prove_normalize_via (axiom-l)prove_normalize.rs:98prove_syntactically_eq (alias)prove_normalize.rs:165zipcombinators.rs:38prove_syntactically_eq (symmetric)prove_normalize.rs:147prove_syntactically_eq (existential-nonvar)prove_normalize.rs:171prove_existential_var_eq (existential-universal)prove_eq.rs:143
prove_after (prove_after)prove_after.rs:20prove_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