Judgment check_fn_in_impl
judgment_fn! {
fn check_fn_in_impl(
program: Program,
env: Env,
impl_assumptions: Predicates,
trait_items: Vec<TraitItem>,
ii_fn: Fn,
crate_id: CrateId,
) => () {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/impls.rs:176
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 |
|---|---|---|
| 188 | ✗ | (if let Some(ti_fn) = trait_items .iter() .downcasted::<Fn>() .find(|trait_f| trait_f.id == ii_fn.id)) |
| 194 | 1 | (super::fns::check_fn(program, env, impl_assumptions, ii_fn, crate_id) => ()) |
| 197 | ✗ | (scope(enter_universally(env, &merge_binders(&ii_fn.binder, &ti_fn.binder)?) => (env, ( FnBoundData { input_args: ii_input_args, output_ty: ii_output_ty, where_clauses: ii_where_clauses, body: _ }, FnBoundData { input_args: ti_input_args, output_ty: ti_output_ty, where_clauses: ti_where_clauses, body: _ }, ))) with() // Prove impl where-clauses follow from trait where-clauses (super::prove_goal(program, env, (impl_assumptions, ti_where_clauses), ii_where_clauses) => ()) // Check argument count matches (if ii_input_args.len() == ti_input_args.len()) // Check each argument: trait arg is subtype of impl arg (contravariance) (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), AtomicPredicate::sub(&ti_input_arg.ty, &ii_input_arg.ty)) => ())) // Check return type: impl return is subtype of trait return (covariance) (super::prove_goal(program, env, (impl_assumptions, ii_where_clauses), AtomicPredicate::sub(ii_output_ty, ti_output_ty)) => ())) |
| ──────── ("check_fn_in_impl") | ||
| 218 | 5 | (check_fn_in_impl(program, env, impl_assumptions, trait_items, ii_fn, crate_id) => ()) |