Positive coverage: is_local_parameter / existential variable
existential variable| Line | Coverage | Source |
|---|---|---|
| ──────── ("existential variable") | ||
| 316 | 1 | (is_local_parameter(_decls, env, _assumptions, TyData::Variable(Variable::ExistentialVar(_))) => Constraints::none(env).ambiguous()) |
1 test exercised this rule:
Source location: crates/formality-rust/src/prove/prove/test/is_local.rs:26
#[test]
fn test_exists_not_local() {
test_prove(
Program::empty(),
term("exists<T> {} => {@IsLocal(Debug(T))}"),
)
.assert_ok(expect!["{Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: false, substitution: {} }}"])
}Proof tree
prove_wc_list (some)prove_wc_list.rs:31prove_wc (trait ref is local)prove_wc.rs:149is_local_trait_ref (local parameter)is_local.rs:225is_local_parameter (existential variable)is_local.rs:315
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24