Judgment can_outlive
judgment_fn! {
/// Check if lt_a can outlive param_b.
/// For non-universal targets, trivially succeeds.
/// For universal lifetime targets, must prove from assumptions.
fn can_outlive(
env: TypeckEnv,
assumptions: Predicates,
outlives: Set<PendingOutlives>,
param_a: Parameter,
param_b: Parameter,
) => () {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/borrow_check/outlives.rs:56
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.
existential target| Line | Coverage | Source |
|---|---|---|
| 73 | ✗ | (if var_b.is_existential()) |
| ──────── ("existential target") | ||
| 75 | 20 | (can_outlive(_env, _assumptions, _outlives, _param_a, var_b: Variable) => ()) |
universal target| Line | Coverage | Source |
|---|---|---|
| 80 | ✗ | (if var_b.is_universal()) |
| 81 | 8 | (prove(&env.program, &env.env, assumptions, AtomicPredicate::outlives(param_a, var_b)) => c) |
| 82 | ✗ | (if c.unconditionally_true()) |
| ──────── ("universal target") | ||
| 84 | 3 | (can_outlive(env, assumptions, _outlives, param_a, var_b: Variable) => ()) |