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
47N/A(let (env, subst) = env.existential_substitution(binder))
48N/A(let via1 = binder.instantiate_with(&subst).unwrap())
501(prove_via(decls, env, assumptions, via1, goal) => c)
──────── ("forall")
522(prove_via(decls, env, assumptions, WcData::ForAll(binder), goal) => c.pop_subst(&subst))

2 tests exercised this rule:

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

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