Test test_a
Source location: crates/formality-rust/src/prove/test/eq_assumptions.rs:15
#[test]
fn test_a() {
test_prove(
Program::empty(),
term("{} => {for<T, U> if {T = u32, U = Vec<T>} U = Vec<u32>}"),
)
.assert_ok(expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}Rules proved (12)
Premises failed (0)
This test records no negative coverage.
Proof trees
Proof tree
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (forall)prove_predicate.rs:36args
scopeprove_predicate.rs:22prove_predicate (implies)prove_predicate.rs:42args
prove_predicate (eq)prove_predicate.rs:116args
prove_eq (normalize-l)prove_eq.rs:70args
prove_normalize (normalize-via-assumption)prove_normalize.rs:37args
prove_normalize_via (axiom-l)prove_normalize.rs:98args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_eq (rigid)prove_eq.rs:48args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (assumption)prove_predicate.rs:49args
prove_via (relation-axiom)prove_via.rs:43args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args