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

Judgment check_fn_in_impl at crates/formality-rust/src/check/impls.rs:178

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
LineCoverageSource
190(if let Some(ti_fn) = trait_items
.iter()
.downcasted::<Fn>()
.find(|trait_f| trait_f.id == ii_fn.id))
196(super::fns::check_fn(program, env, impl_assumptions, ii_fn, crate_id) => ())
199(let (env, (ii_bound, ti_bound)) = env.instantiate_universally(&merge_binders(&ii_fn.binder, &ti_fn.binder)?))
200N/A(let FnBoundData { input_args: ii_input_args, output_ty: ii_output_ty, where_clauses: ii_where_clauses, body: _ } = ii_bound)
201N/A(let FnBoundData { input_args: ti_input_args, output_ty: ti_output_ty, where_clauses: ti_where_clauses, body: _ } = ti_bound)
204(super::prove_goal(program, &env, (&impl_assumptions, &ti_where_clauses), &ii_where_clauses) => ())
207(if ii_input_args.len() == ti_input_args.len())
210(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), Predicate::sub(&ti_input_arg.ty, &ii_input_arg.ty)) => ()))
215(super::prove_goal(program, &env, (&impl_assumptions, &ii_where_clauses), Predicate::sub(ii_output_ty, ti_output_ty)) => ())
──────── ("check_fn_in_impl")
218(check_fn_in_impl(program, env, impl_assumptions, trait_items, ii_fn, crate_id) => ())