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_predicate / trait implied bound

trait implied bound
LineCoverageSource
10619(ti in decls.trait_invariants())
107✗(scope(enter_existentially_with_constraints(env, &ti.binder) => (env, ti)) with(c)
(prove_via(decls, env, assumptions, &ti.where_clause, trait_ref) => c)
(prove_after(decls, c, assumptions, &ti.trait_ref) => c))
──────── ("trait implied bound")
1111(prove_predicate(decls, env, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => c)

1 test exercised this rule:

Source location: crates/formality-rust/src/prove/test/eq_partial_eq.rs:25 (all coverage from this test)

#[test]
fn eq_implies_partial_eq() {
    let assumptions: Predicates = Predicates::t();
    let goal: Predicate = 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: {} }}"]);
}
Proof tree

How to read this page