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

Positive coverage: check_fn_in_impl / check_fn_in_impl

check_fn_in_impl
LineCoverageSource
188✗(if let Some(ti_fn) = trait_items
.iter()
.downcasted::<Fn>()
.find(|trait_f| trait_f.id == ii_fn.id))
1941(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")
2185(check_fn_in_impl(program, env, impl_assumptions, trait_items, ii_fn, crate_id) => ())

5 tests exercised this rule:

Source location: tests/drop.rs:23 (all coverage from this test)

Proof tree
… (200 of 3538 nodes shown)

Source location: tests/drop.rs:43 (all coverage from this test)

Proof tree
… (200 of 3630 nodes shown)

Source location: tests/drop.rs:61 (all coverage from this test)

Proof tree
… (200 of 3579 nodes shown)

Source location: tests/drop.rs:108 (all coverage from this test)

Proof tree
… (200 of 3529 nodes shown)

Source location: tests/drop.rs:128 (all coverage from this test)

Proof tree
… (200 of 3541 nodes shown)

How to read this page