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:22: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 216) | 12 tests |
| is_local_trait_ref | local parameter | is_local_parameter(decls, env, assumptions, &goa… (line 224) | 12 tests |
| is_local_parameter | local parameter | prove_normalize(decls, env, assumptions, goal) =… (line 305) | 12 tests |
| prove_predicate | forall | scope(enter_universally_with_constraints(env, bi… (line 34, blamed at line 35) | not counted by the judgment view |
| prove_predicate | trait ref is local | is_local_trait_ref(decls, env, assumptions, trai… (line 136) | 12 tests |
| prove_predicate_list | some | prove_predicate(decls, env, assumptions, wc0) =>… (line 26) | 67 tests |
Proof trees
Failed proof tree
prove failedtest_util.rs:57args
ruletest_util.rs:57prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "forall"prove_predicate.rs:35prove_predicate failedprove_predicate.rs:22args
rule "trait ref is local"prove_predicate.rs:136is_local_trait_ref failedis_local.rs:206args
rule "local parameter"is_local.rs:224is_local_parameter failedis_local.rs:293args
rule "local parameter"is_local.rs:305prove_normalize failedprove_normalize.rs:22args
rule "local trait"is_local.rs:216 (failed: if_false)