Test test_normalize_assoc_ty_existential0
Source location: crates/formality-rust/src/prove/test/eq_assumptions.rs:41
#[test]
fn test_normalize_assoc_ty_existential0() {
test_prove(
Program::empty(),
term("exists<A> {} => {for<T> if { <T as Iterator>::Item = u32 } <A as Iterator>::Item = u32}"),
).assert_err(
expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: <?ty_0 as Iterator>::Item = u32, via: <!ty_1 as Iterator>::Item = u32, assumptions: {<!ty_1 as Iterator>::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }
the rule "existential-nonvar" at (prove_eq.rs) failed because
pattern `None` did not match value `Some(!ty_1)`
the rule "existential-universal" at (prove_eq.rs) failed because
condition evaluated to false: `env.universe(p) < env.universe(v)`
the rule "existential-nonvar" at (prove_eq.rs) failed because
pattern `None` did not match value `Some(!ty_1)`
the rule "existential-universal" at (prove_eq.rs) failed because
condition evaluated to false: `env.universe(p) < env.universe(v)`
the rule "normalize-via-impl" at (prove_normalize.rs) failed because
expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: <!ty_0 as Iterator>::Item = <?ty_1 as Iterator>::Item, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !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 = ?ty_1, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
the rule "existential-nonvar" at (prove_eq.rs) failed because
pattern `None` did not match value `Some(!ty_0)`
the rule "existential-universal" at (prove_eq.rs) failed because
condition evaluated to false: `env.universe(p) < env.universe(v)`
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: ?ty_1, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !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: u32 = <?ty_1 as Iterator>::Item, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
the rule "existential-nonvar" at (prove_eq.rs) failed because
pattern `None` did not match value `Some(!ty_0)`
the rule "existential-universal" at (prove_eq.rs) failed because
condition evaluated to false: `env.universe(p) < env.universe(v)`
the rule "existential-nonvar" at (prove_eq.rs) failed because
pattern `None` did not match value `Some(!ty_0)`
the rule "existential-universal" at (prove_eq.rs) failed because
condition evaluated to false: `env.universe(p) < env.universe(v)`
the rule "normalize-via-impl" at (prove_normalize.rs) failed because
expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: ?ty_1 = !ty_0, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
the rule "existential-nonvar" at (prove_eq.rs) failed because
pattern `None` did not match value `Some(!ty_0)`
the rule "existential-universal" at (prove_eq.rs) failed because
condition evaluated to false: `env.universe(p) < env.universe(v)`
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: ?ty_1, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
the rule "existential-nonvar" at (prove_eq.rs) failed because
pattern `None` did not match value `Some(!ty_0)`
the rule "existential-universal" at (prove_eq.rs) failed because
condition evaluated to false: `env.universe(p) < env.universe(v)`
the rule "existential-nonvar" at (prove_eq.rs) failed because
pattern `None` did not match value `Some(!ty_0)`
the rule "existential-universal" at (prove_eq.rs) failed because
condition evaluated to false: `env.universe(p) < env.universe(v)`
the rule "normalize-via-impl" at (prove_normalize.rs) failed because
expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`"#]]);
}Rules proved (0)
This test records no positive coverage.
Premises failed (19)
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 | alias | prove(decls, env, assumptions, Predicates::all_e… (line 56) | 1 test |
| prove_eq | existential | prove_existential_var_eq(decls, env, assumptions… (line 62) | 5 tests |
| prove_eq | normalize-l | prove_normalize(decls, env, assumptions, x) => C… (line 68) | 17 tests |
| prove_eq | normalize-l | prove_after(decls, c, assumptions, eq(y, z)) => … (line 69) | 3 tests |
| prove_existential_var_eq | existential-nonvar | if let None = t.downcast::<Variable>() (line 94) | 2 tests |
| prove_existential_var_eq | existential-universal | if env.universe(p) < env.universe(v) (line 140) | 2 tests |
| prove_normalize | normalize-via-assumption | prove_normalize_via(decls, env, assumptions, a, … (line 36) | 14 tests |
| prove_normalize | normalize-via-impl | decl in decls.alias_eq_decls(&a.name) (line 42) | 1 test |
| prove_normalize_via | axiom-l | prove_syntactically_eq(decls, env, assumptions, … (line 96) | 1 test |
| prove_syntactically_eq | symmetric | prove_syntactically_eq(decls, env, assumptions, … (line 143) | 1 test |
| prove_syntactically_eq | alias | zip(decls, env, assumptions, a_parameters.clone(… (line 161) | 1 test |
| prove_syntactically_eq | existential-nonvar | prove_existential_var_eq(decls, env, assumptions… (line 167) | 1 test |
| prove_predicate | forall | scope(enter_universally_with_constraints(env, bi… (line 34, blamed at line 35) | not counted by the judgment view |
| prove_predicate | implies | prove_predicate(decls, env, (assumptions, p1), p… (line 41) | 3 tests |
| prove_predicate | assumption | prove_via(decls, env, assumptions, a, goal) => c (line 48) | 34 tests |
| 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 "implies"prove_predicate.rs:41prove_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 "axiom-l"prove_normalize.rs:96prove_syntactically_eq failedprove_normalize.rs:130args
rule "alias"prove_normalize.rs:161prove_syntactically_eq failedprove_normalize.rs:130args
rule "symmetric"prove_normalize.rs:143prove_syntactically_eq failedprove_normalize.rs:130args
rule "existential-nonvar"prove_normalize.rs:167prove_existential_var_eq failedprove_eq.rs:76args
rule "existential-nonvar"prove_eq.rs:94 (failed: if_let)rule "existential-universal"prove_eq.rs:140 (failed: if_false)
rule "symmetric"prove_normalize.rs:143prove_syntactically_eq failedprove_normalize.rs:130args
rule "alias"prove_normalize.rs:161prove_syntactically_eq failedprove_normalize.rs:130args
rule "existential-nonvar"prove_normalize.rs:167prove_existential_var_eq failedprove_eq.rs:76args
rule "existential-nonvar"prove_eq.rs:94 (failed: if_let)rule "existential-universal"prove_eq.rs:140 (failed: if_false)
rule "normalize-via-impl"prove_normalize.rs:42 (failed: empty_collection)
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:69prove_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 "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "alias"prove_eq.rs:56prove failedprove_eq.rs:56args
ruleprove_eq.rs:56prove_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 "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "existential"prove_eq.rs:62prove_existential_var_eq failedprove_eq.rs:76args
rule "existential-nonvar"prove_eq.rs:94 (failed: if_let)rule "existential-universal"prove_eq.rs:140 (failed: if_false)
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 "normalize-l"prove_eq.rs:69prove_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 "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
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 "axiom-l"prove_normalize.rs:96prove_syntactically_eq failedprove_normalize.rs:130args
rule "alias"prove_normalize.rs:161prove_syntactically_eq failedprove_normalize.rs:130args
rule "symmetric"prove_normalize.rs:143prove_syntactically_eq failedprove_normalize.rs:130args
rule "existential-nonvar"prove_normalize.rs:167prove_existential_var_eq failedprove_eq.rs:76args
rule "existential-nonvar"prove_eq.rs:94 (failed: if_let)rule "existential-universal"prove_eq.rs:140 (failed: if_false)
rule "symmetric"prove_normalize.rs:143prove_syntactically_eq failedprove_normalize.rs:130args
rule "alias"prove_normalize.rs:161prove_syntactically_eq failedprove_normalize.rs:130args
rule "existential-nonvar"prove_normalize.rs:167prove_existential_var_eq failedprove_eq.rs:76args
rule "existential-nonvar"prove_eq.rs:94 (failed: if_let)rule "existential-universal"prove_eq.rs:140 (failed: if_false)
rule "normalize-via-impl"prove_normalize.rs:42 (failed: empty_collection)
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "alias"prove_eq.rs:56prove failedprove_eq.rs:56args
ruleprove_eq.rs:56prove_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 "existential"prove_eq.rs:62prove_existential_var_eq failedprove_eq.rs:76args
rule "existential-nonvar"prove_eq.rs:94 (failed: if_let)rule "existential-universal"prove_eq.rs:140 (failed: if_false)
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 "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 "axiom-l"prove_normalize.rs:96prove_syntactically_eq failedprove_normalize.rs:130args
rule "alias"prove_normalize.rs:161prove_syntactically_eq failedprove_normalize.rs:130args
rule "symmetric"prove_normalize.rs:143prove_syntactically_eq failedprove_normalize.rs:130args
rule "existential-nonvar"prove_normalize.rs:167prove_existential_var_eq failedprove_eq.rs:76args
rule "existential-nonvar"prove_eq.rs:94 (failed: if_let)rule "existential-universal"prove_eq.rs:140 (failed: if_false)
rule "symmetric"prove_normalize.rs:143prove_syntactically_eq failedprove_normalize.rs:130args
rule "alias"prove_normalize.rs:161prove_syntactically_eq failedprove_normalize.rs:130args
rule "existential-nonvar"prove_normalize.rs:167prove_existential_var_eq failedprove_eq.rs:76args
rule "existential-nonvar"prove_eq.rs:94 (failed: if_let)rule "existential-universal"prove_eq.rs:140 (failed: if_false)
rule "normalize-via-impl"prove_normalize.rs:42 (failed: empty_collection)