Positive coverage: prove_via / predicate-congruence-axiom

13 tests exercised this rule:

Source location: crates/formality-rust/src/prove/prove/test/eq_partial_eq.rs:25

#[test]
fn eq_implies_partial_eq() {
    let assumptions: Wcs = Wcs::t();
    let goal: Wc = term("for<T> if {Eq(T)} PartialEq(T)");
    let constraints = prove(decls(), (), assumptions, goal);
    constraints.assert_ok(
    expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}

Source location: tests/basic_tests.rs:58

#[test]
fn hello_world() {
    FormalityTest::new(crates![crate Foo {
        trait Foo<T> where T: Bar<Self>, Self: Baz {}

        trait Bar<T> where T: Baz {}

        trait Baz {}

        impl Baz for u32 {}

        impl Bar<u32> for u32 {}
        impl<T> Bar<T> for () where T: Baz {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/basic_tests.rs:149

#[test]
fn non_lifetime_binder_in_trait_impl_where_clause_pass() {
    FormalityTest::new(crates![crate core {
        #![feature(non_lifetime_binders)]
        trait A<T> where T: B { }

        trait B { }

        impl<T> B for T where for<U> u32: A<U> { }
    }])
    .skip_execute()
    .ok()
}

Source location: tests/basic_tests.rs:179

#[test]
fn non_lifetime_binder_in_neg_trait_impl_where_clause_pass() {
    FormalityTest::new(crates![crate core {
        #![feature(non_lifetime_binders)]
        trait A<T> where T: B { }

        trait B { }

        impl<T> !A<T> for u32 where for<U> u32: A<U> { }

        impl <T> B for T {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/coherence_overlap.rs:147

#[test]
fn neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
    FormalityTest::new(crates![crate core {
        trait CoreTrait {}
        struct CoreStruct {}
        impl !CoreTrait for CoreStruct {}
    },
    crate foo {
        trait FooTrait {}
        impl<T> FooTrait for T where T: CoreTrait {}
        impl FooTrait for CoreStruct {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/coherence_overlap.rs:206

#[test]
fn u32_T_where_T_Not_impls() {
    FormalityTest::new(crates![crate core {
        trait Foo {}
        impl Foo for u32 {}
        impl<T> Foo for T where T: Not {}

        trait Not {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/coherence_overlap.rs:307

#[test]
fn is_local_unknowable_trait_ref() {
    FormalityTest::new(crates![crate core {
        trait Project {
            type Assoc: [];
        }

        impl<T> Project for T {
            type Assoc = T;
        }

        trait Foo<U> { }
    },
    crate foo {
        struct LocalType {}

        trait Overlap<U> {}
        impl<T, U> Overlap<U> for T
        where
            <T as Project>::Assoc: Foo<U> {}
        impl<T> Overlap<LocalType> for () {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/consts.rs:23

#[test]
fn ok() {
    FormalityTest::new(crates![crate Foo {
        trait Foo<const C> where type_of_const C is bool {}
        trait Bar<const C> where type_of_const C is u32 {}

        impl<const C> Foo<C> for u32 where type_of_const C is bool {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/consts.rs:92

#[test]
fn generic_match() {
    FormalityTest::new(crates![crate Foo {
        trait Foo<const C> where type_of_const C is bool {}

        // Here, the impl matches the trait bound.
        impl<const C> Foo<C> for u32 where type_of_const C is bool {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/drop.rs:38

#[test]
fn drop_impl_generic_struct() {
    FormalityTest::new(crates![
        crate Foo {
            trait Clone {}

            struct MyStruct<T> where T: Clone {
                value: T,
            }

            impl<T> Drop for MyStruct<T> where T: Clone {}
        }
    ])
    .skip_execute()
    .ok()
}

Source location: tests/mir_typeck.rs:729

fn foo<'a, T>(v1: &'a T) -> T
where
    T: Copy,
    T: 'a,
{
    exists<'r0> {
        let v2: T = *v1;
        return v2;
    }
}

Proof trees omitted for the remaining 3 tests.

Source location: tests/references.rs:36

Source location: tests/well_formed_trait_ref.rs:19

#[test]
fn dependent_where_clause() {
    FormalityTest::new(crates![crate foo {
        trait Trait1 {}

        trait Trait2 {}

        struct S1<T> where T: Trait1 {
            dummy: T,
        }

        struct S2<T> where T: Trait1, S1<T> : Trait2 {
            dummy: T,
        }
    }])
    .skip_execute()
    .ok()
}