Judgment check_associated_ty_value at crates/formality-rust/src/check/impls.rs:196
Signature:
check_associated_ty_value(program: Program, impl_env: Env, impl_assumptions: Wcs, trait_items: Vec<TraitItem>, impl_value: AssociatedTyValue,) => ()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 |
|---|---|---|
| 206 | N/A | (let AssociatedTyValue { id, binder } = &impl_value) |
| 209 | ✗ | (if let Some(trait_associated_ty) = trait_items .iter() .downcasted::<AssociatedTy>() .find(|trait_associated_ty| trait_associated_ty.id == *id)) |
| 215 | ✗ | (let (env, (ii_bound, ti_bound)) = impl_env.instantiate_universally(&merge_binders(binder, &trait_associated_ty.binder)?)) |
| 216 | N/A | (let AssociatedTyValueBoundData { where_clauses: ii_where_clauses, ty: ii_ty } = ii_bound) |
| 217 | N/A | (let AssociatedTyBoundData { ensures: ti_ensures, where_clauses: ti_where_clauses } = ti_bound) |
| 220 | ✗ | (super::where_clauses::prove_where_clauses_well_formed(program, &env, (&impl_assumptions, &ii_where_clauses), &ii_where_clauses) => ()) |
| 223 | ✗ | (super::prove_goal(program, &env, (&impl_assumptions, &ti_where_clauses), &ii_where_clauses) => ()) |
| 226 | ✗ | (super::prove_goal(program, env, (impl_assumptions, ii_where_clauses), Relation::well_formed(ii_ty)) => ()) |
| 229 | N/A | (let ensures: Wcs = ti_ensures.iter().map(|e| e.to_wc(&ii_ty)).collect()) |
| 230 | ✗ | (super::prove_goal(program, &env, (&impl_assumptions, &ii_where_clauses), ensures) => ()) |
| ──────── ("check_associated_ty_value") | ||
| 233 | 98 | (check_associated_ty_value(program, impl_env, impl_assumptions, trait_items, impl_value) => ()) |