Test test_forall_not_local
Source location: crates/formality-rust/src/prove/test/is_local.rs:11
#[test]
fn test_forall_not_local() {
test_prove(Program::empty(), term("{} => {for<T> @IsLocal(Debug(T))}")).assert_err(expect![[r#"
crates/formality-rust/src/prove/prove_normalize.rs:18:1: no applicable rules for prove_normalize { p: !ty_1, assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }
the rule "local trait" at (is_local.rs) failed because
condition evaluated to false: `decls.is_local_trait_id(&goal.trait_id)`
decls = program([], 222)
&goal.trait_id = Debug"#]]);
}
Rules proved (0)
This test records no positive coverage.
Premises failed (6)
The last column links to the premise’s page when the judgment view counts this failure against that premise. It does not when the premise is read as infallible, or when the failure was blamed inside a multi-line premise that carries no record on its own first line.
| Judgment | Rule | Premise | All tests of this premise |
|---|---|---|---|
| is_local_trait_ref | local trait | if decls.is_local_trait_id(&goal.trait_id) (line 207) | 7 tests |
| is_local_trait_ref | local parameter | is_local_parameter(decls, env, assumptions, &goa… (line 215) | 7 tests |
| is_local_parameter | local parameter | prove_normalize(decls, env, assumptions, goal) =… (line 287) | 7 tests |
| prove_wc | forall | prove_wc(decls, env, assumptions, p1) => c (line 35) | 8 tests |
| prove_wc | trait ref is local | is_local_trait_ref(decls, env, assumptions, trai… (line 140) | 7 tests |
| prove_wc_list | some | prove_wc(decls, env, assumptions, wc0) => c (line 26) | 42 tests |
Proof trees
Failed proof tree
prove failedtest_util.rs:57args
ruletest_util.rs:57prove_wc_list failedprove_wc_list.rs:8args
rule "some"prove_wc_list.rs:26prove_wc failedprove_wc.rs:21args
rule "forall"prove_wc.rs:35prove_wc failedprove_wc.rs:21args
rule "trait ref is local"prove_wc.rs:140is_local_trait_ref failedis_local.rs:197args
rule "local parameter"is_local.rs:215is_local_parameter failedis_local.rs:275args
rule "local parameter"is_local.rs:287prove_normalize failedprove_normalize.rs:18args
rule "local trait"is_local.rs:207 (failed: if_false)