Test all_t_not_copy
Source location: crates/formality-rust/src/prove/test/magic_copy.rs:40
#[test]
fn all_t_not_copy() {
test_prove(decls(), term("{} => {for<T> Copy(T)}")).assert_err(
expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}Rules proved (0)
This test records no positive coverage.
Premises failed (12)
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 |
|---|---|---|---|
| prove_after | prove_after | prove(decls, c1.env(), assumptions, goal) => c2 (line 19) | 21 tests |
| prove_eq | symmetric | prove_eq(decls, env, assumptions, r, l) => env_c (line 38) | 17 tests |
| prove_eq | normalize-l | prove_normalize(decls, env, assumptions, x) => C… (line 68) | 17 tests |
| prove_normalize | normalize-via-assumption | prove_normalize_via(decls, env, assumptions, a, … (line 36) | 14 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 | assumption | prove_via(decls, env, assumptions, a, goal) => c (line 48) | 34 tests |
| prove_predicate | positive impl | scope(enter_existentially_with_constraints(env, … (line 60, blamed at line 71) | not counted by the judgment view |
| prove_predicate | positive impl | scope(enter_existentially_with_constraints(env, … (line 60, blamed at line 78) | not counted by the judgment view |
| prove_predicate | trait implied bound | scope(enter_existentially_with_constraints(env, … (line 107, blamed at line 108) | not counted by the judgment view |
| prove_predicate | trait implied bound | scope(enter_existentially_with_constraints(env, … (line 107, blamed at line 109) | not counted by the judgment view |
| prove_predicate | eq | prove_eq(decls, env, assumptions, a, b) => c (line 115) | 17 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 "positive impl"prove_predicate.rs:71prove failedprove_predicate.rs:71args
ruleprove_predicate.rs:71prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "trait implied bound"prove_predicate.rs:109prove_after failedprove_after.rs:8args
rule "prove_after"prove_after.rs:19prove failedprove_after.rs:19args
ruleprove_after.rs:19prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "positive impl"prove_predicate.rs:78prove_after failedprove_after.rs:8args
rule "prove_after"prove_after.rs:19prove failedprove_after.rs:19args
ruleprove_after.rs:19prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "positive impl"prove_predicate.rs:71prove failedprove_predicate.rs:71args
ruleprove_predicate.rs:71prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "trait implied bound"prove_predicate.rs:108prove_via failedprove_via.rs:9args