Test for_t_exists_u

Source location: crates/formality-rust/src/prove/test/universes.rs:37

#[test]
fn for_t_exists_u() {
    let decls = Program {
        crates: Arc::new(Program::program_from_items(vec![
            term("trait Test<T> where {}"),
            term("impl<X> Test<X> for X {}"),
        ])),
        ..Program::empty()
    };

    test_prove(decls, term("{} => {for<T> Test(T, T)}")).assert_ok(expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}

Rules proved (9)

Premises failed (0)

This test records no negative coverage.

Proof trees