Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Positive coverage: prove_via / forall

forall
LineCoverageSource
49✗(scope(enter_existentially_with_constraints(env, binder) => (env, via1)) with(c)
// Try to prove `T: Trait<?a> == goal`.
(prove_via(decls, env, assumptions, via1, goal) => c))
──────── ("forall")
532(prove_via(decls, env, assumptions, Predicate::ForAll(binder), goal) => c)

2 tests exercised this rule:

Source location: tests/basic_tests.rs:149 (all coverage from this test)

#[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()
}
Proof tree

Source location: tests/basic_tests.rs:179 (all coverage from this test)

#[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()
}
Proof tree

How to read this page