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

trait implied bound
LineCoverageSource
11712(ti in decls.trait_invariants())
118N/A(let (env, subst) = env.existential_substitution(&ti.binder))
119N/A(let ti = ti.binder.instantiate_with(&subst).unwrap())
1204(prove_via(decls, env, assumptions, &ti.where_clause, trait_ref) => c)
1213(prove_after(decls, c, assumptions, &ti.trait_ref) => c)
──────── ("trait implied bound")
1231(prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))

1 test 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: {} }}"]);
}
Proof tree