Judgment loan_not_required_by_parameters
judgment_fn! {
/// For some `place_live` which has type `place_live_ty` where
///
/// let x = &'lt_loan place_borrowed;
/// ...
/// access(place_accessed); // conflicts with the borrow
/// ...
/// access(place_live) // <-- an access like this occurs later
///
/// ...show that `place_live_ty` does not require data derived from `x`.
fn loan_not_required_by_parameters(
env: TypeckEnv,
assumptions: Predicates,
outlives: Set<PendingOutlives>,
loan: Loan,
live_parameters: Vec<Parameter>,
) => () {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/borrow_check/nll.rs:1533
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.
loan_not_required_by_parameters| Line | Coverage | Source |
|---|---|---|
| 1553 | ✗ | (for_all(param in live_parameters) (loan_not_required_by_parameter(env, assumptions, outlives, loan, param) => ())) |
| ──────── ("loan_not_required_by_parameters") | ||
| 1556 | 12 | (loan_not_required_by_parameters(env, assumptions, outlives, loan, live_parameters) => ()) |