Judgment check_fn_in_impl at crates/formality-rust/src/check/impls.rs:151
Signature:
check_fn_in_impl(program: Program, env: Env, impl_assumptions: Wcs, trait_items: Vec<TraitItem>, ii_fn: Fn, crate_id: CrateId,) => ()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_fn_in_impl| Line | Coverage | Source |
|---|---|---|
| 163 | ✗ | (if let Some(ti_fn) = trait_items .iter() .downcasted::<Fn>() .find(|trait_f| trait_f.id == ii_fn.id)) |
| 169 | ✗ | (super::fns::check_fn(program, env, impl_assumptions, ii_fn, crate_id) => ()) |
| 172 | ✗ | (let (env, (ii_bound, ti_bound)) = env.instantiate_universally(&merge_binders(&ii_fn.binder, &ti_fn.binder)?)) |
| 173 | N/A | (let FnBoundData { input_args: ii_input_args, output_ty: ii_output_ty, where_clauses: ii_where_clauses, body: _ } = ii_bound) |
| 174 | N/A | (let FnBoundData { input_args: ti_input_args, output_ty: ti_output_ty, where_clauses: ti_where_clauses, body: _ } = ti_bound) |
| 177 | ✗ | (super::prove_goal(program, &env, (&impl_assumptions, &ti_where_clauses), &ii_where_clauses) => ()) |
| 180 | ✗ | (if ii_input_args.len() == ti_input_args.len()) |
| 183 | ✗ | (for_all(pair in ii_input_args.iter().zip(ti_input_args.iter())) (let (ii_input_arg, ti_input_arg) = pair) (super::prove_goal(program, &env, (&impl_assumptions, &ii_where_clauses), Relation::sub(&ti_input_arg.ty, &ii_input_arg.ty)) => ())) |
| 188 | ✗ | (super::prove_goal(program, &env, (&impl_assumptions, &ii_where_clauses), Relation::sub(ii_output_ty, ti_output_ty)) => ()) |
| ──────── ("check_fn_in_impl") | ||
| 191 | ✗ | (check_fn_in_impl(program, env, impl_assumptions, trait_items, ii_fn, crate_id) => ()) |