Judgment may_contain_downstream_type at crates/formality-rust/src/prove/is_local.rs:132
Signature:
may_contain_downstream_type(_decls: Program, env: Env, assumptions: Wcs, parameter: Parameter,) => ()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.
existential variable| Line | Coverage | Source |
|---|---|---|
| ──────── ("existential variable") | ||
| 145 | ✗ | (may_contain_downstream_type(_decls, _env, _assumptions, TyData::Variable(Variable::ExistentialVar(_))) => ()) |
rigid type parameter| Line | Coverage | Source |
|---|---|---|
| 151 | ✗ | (p in parameters.iter()) |
| 152 | ✗ | (may_contain_downstream_type(decls, env, assumptions, p) => ()) |
| ──────── ("rigid type parameter") | ||
| 154 | ✗ | (may_contain_downstream_type(decls, env, assumptions, RigidTy { name: _, parameters }) => ()) |
via normalize| Line | Coverage | Source |
|---|---|---|
| 160 | ✗ | (prove_normalize(decls, env, assumptions, parameter) => Constrained(p, c)) |
| 161 | N/A | (let assumptions = c.substitution().apply(assumptions)) |
| 162 | ✗ | (may_contain_downstream_type(decls, env, assumptions, p) => ()) |
| ──────── ("via normalize") | ||
| 164 | ✗ | (may_contain_downstream_type(decls, env, assumptions, parameter) => ()) |
forall| Line | Coverage | Source |
|---|---|---|
| 169 | N/A | (let (env, ty) = env.instantiate_existentially(binder)) |
| 170 | ✗ | (may_contain_downstream_type(decls, env, assumptions, ty) => ()) |
| ──────── ("forall") | ||
| 172 | ✗ | (may_contain_downstream_type(decls, env, assumptions, TyData::PredicateTy(PredicateTy::ForAll(binder))) => ()) |