Judgment prove_normalize
judgment_fn! {
/// Normalize `p` one step, returning a set of constraints and a new parameter `q` that is
/// semantically equivalent to `p`. e.g., if p is `<Vec<T> as IntoIterator>::Item`, this would
/// return `T`.
pub fn prove_normalize(
_decls: Program,
env: Env,
assumptions: Predicates,
p: Parameter,
) => Constrained<Parameter> {
/* rules omitted */
}
}Source: crates/formality-rust/src/prove/prove_normalize.rs:22
No applicable rule observed: at least one test exercised this judgment with no matching rule.
The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.
normalize-via-assumption| Line | Coverage | Source |
|---|---|---|
| 35 | ✗ | (a in assumptions) |
| 36 | 14 | (prove_normalize_via(decls, env, assumptions, a, goal) => c) |
| ──────── ("normalize-via-assumption") | ||
| 38 | 4 | (prove_normalize(decls, env, assumptions, goal) => c) |
normalize-via-impl| Line | Coverage | Source |
|---|---|---|
| 42 | 1 | (decl in decls.alias_eq_decls(&a.name)) |
| 43 | ✗ | (scope(enter_existentially_with_constraints(env, &decl.binder) => (env, AliasEqDeclBoundData { alias: AliasTy { name, parameters }, ty, where_clause })) with(ty, c) (assert a.name == *name) (prove(decls, env, assumptions, Predicates::all_eq(&a.parameters, ¶meters)) => c) (prove_after(decls, c, assumptions, &where_clause) => c) (let ty = c.substitution().apply(ty))) |
| ──────── ("normalize-via-impl") | ||
| 50 | 55 | (prove_normalize(decls, env, assumptions, Ty::AliasTy(a)) => Constrained(ty, c)) |