Judgment prove_normalize at crates/formality-rust/src/prove/prove/prove/prove_normalize.rs:19
Signature:
prove_normalize(_decls: Program, env: Env, assumptions: Wcs, p: Parameter,) => Constrained<Parameter>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 |
|---|---|---|
| 32 | ✗ | (a in assumptions) |
| 33 | 9 | (prove_normalize_via(decls, env, assumptions, a, goal) => c) |
| ──────── ("normalize-via-assumption") | ||
| 35 | 3 | (prove_normalize(decls, env, assumptions, goal) => c) |
normalize-via-impl| Line | Coverage | Source |
|---|---|---|
| 39 | 1 | (decl in decls.alias_eq_decls(&a.name)) |
| 40 | N/A | (let (env, subst) = env.existential_substitution(&decl.binder)) |
| 41 | N/A | (let decl = decl.binder.instantiate_with(&subst).unwrap()) |
| 42 | N/A | (let AliasEqDeclBoundData { alias: AliasTy { name, parameters }, ty, where_clause } = decl) |
| 43 | ✗ | (assert a.name == *name) |
| 44 | ✗ | (prove(decls, env, assumptions, Wcs::all_eq(&a.parameters, ¶meters)) => c) |
| 45 | ✗ | (prove_after(decls, c, assumptions, &where_clause) => c) |
| 46 | N/A | (let ty = c.substitution().apply(ty)) |
| 47 | N/A | (let c = c.pop_subst(&subst)) |
| 48 | ✗ | (assert c.env().encloses(&ty)) |
| ──────── ("normalize-via-impl") | ||
| 50 | 27 | (prove_normalize(decls, env, assumptions, TyData::AliasTy(a)) => Constrained(ty, c)) |