Test test_b
Source location: crates/formality-rust/src/prove/test/eq_assumptions.rs:24
#[test]
fn test_b() {
test_prove(
Program::empty(),
term("exists<A> {} => {for<T, U> if {T = u32, U = Vec<T>} A = U}"),
)
.assert_ok(expect!["{Constraints { env: Env { variables: [?ty_2, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => Vec<u32>, ?ty_2 => u32} }}"]);
}
Rules proved (12)
Premises failed (0)
This test records no negative coverage.
Proof trees
Proof tree
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (forall)prove_wc.rs:36args
prove_wc (implies)prove_wc.rs:42args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (normalize-l)prove_eq.rs:70args
prove_normalize (normalize-via-assumption)prove_normalize.rs:33args
prove_normalize_via (axiom-l)prove_normalize.rs:97args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (normalize-l)prove_eq.rs:70args
prove_normalize (normalize-via-assumption)prove_normalize.rs:33args
prove_normalize_via (axiom-l)prove_normalize.rs:97args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args