Judgment may_contain_downstream_type at crates/formality-rust/src/prove/prove/prove/is_local.rs:136
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") | ||
| 149 | ✗ | (may_contain_downstream_type(_decls, _env, _assumptions, TyData::Variable(Variable::ExistentialVar(_))) => ()) |
rigid type parameter| Line | Coverage | Source |
|---|---|---|
| 155 | ✗ | (p in parameters.iter()) |
| 156 | ✗ | (may_contain_downstream_type(decls, env, assumptions, p) => ()) |
| ──────── ("rigid type parameter") | ||
| 158 | ✗ | (may_contain_downstream_type(decls, env, assumptions, RigidTy { name: _, parameters }) => ()) |
via normalize| Line | Coverage | Source |
|---|---|---|
| 164 | ✗ | (prove_normalize(decls, env, assumptions, parameter) => Constrained(p, c)) |
| 165 | N/A | (let assumptions = c.substitution().apply(assumptions)) |
| 166 | ✗ | (may_contain_downstream_type(decls, env, assumptions, p) => ()) |
| ──────── ("via normalize") | ||
| 168 | ✗ | (may_contain_downstream_type(decls, env, assumptions, parameter) => ()) |
forall| Line | Coverage | Source |
|---|---|---|
| 173 | N/A | (let (env, ty) = env.instantiate_existentially(binder)) |
| 174 | ✗ | (may_contain_downstream_type(decls, env, assumptions, ty) => ()) |
| ──────── ("forall") | ||
| 176 | ✗ | (may_contain_downstream_type(decls, env, assumptions, TyData::PredicateTy(PredicateTy::ForAll(binder))) => ()) |