Judgment check_associated_ty_value
judgment_fn! {
fn check_associated_ty_value(
program: Program,
impl_env: Env,
impl_assumptions: Predicates,
trait_items: Vec<TraitItem>,
impl_value: AssociatedTyValue,
) => () {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/impls.rs:223
The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.
check_associated_ty_value| Line | Coverage | Source |
|---|---|---|
| 233 | N/A | (let AssociatedTyValue { id, binder } = &impl_value) |
| 236 | ✗ | (if let Some(trait_associated_ty) = trait_items .iter() .downcasted::<AssociatedTy>() .find(|trait_associated_ty| trait_associated_ty.id == *id)) |
| 242 | ✗ | (scope(enter_universally(impl_env, &merge_binders(binder, &trait_associated_ty.binder)?) => (env, ( AssociatedTyValueBoundData { where_clauses: ii_where_clauses, ty: ii_ty }, AssociatedTyBoundData { ensures: ti_ensures, where_clauses: ti_where_clauses }, ))) with() // Prove impl where-clauses are well-formed (super::where_clauses::prove_where_clauses_well_formed(program, env, (impl_assumptions, ii_where_clauses), ii_where_clauses) => ()) // Prove impl where-clauses follow from trait where-clauses (super::prove_goal(program, env, (impl_assumptions, ti_where_clauses), ii_where_clauses) => ()) // Prove the impl type is well-formed (super::prove_goal(program, env, (impl_assumptions, ii_where_clauses), AtomicPredicate::well_formed(ii_ty)) => ()) // Prove the ensures clauses (let ensures: Predicates = ti_ensures.iter().map(|e| e.to_predicate(ii_ty)).collect()) (super::prove_goal(program, env, (impl_assumptions, ii_where_clauses), ensures) => ())) |
| ──────── ("check_associated_ty_value") | ||
| 262 | 194 | (check_associated_ty_value(program, impl_env, impl_assumptions, trait_items, impl_value) => ()) |