Judgment may_contain_downstream_type
judgment_fn! {
fn may_contain_downstream_type(
_decls: Program,
env: Env,
assumptions: Predicates,
parameter: Parameter,
) => () {
/* rules omitted */
}
}Source: crates/formality-rust/src/prove/is_local.rs:141
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") | ||
| 154 | ✗ | (may_contain_downstream_type(_decls, _env, _assumptions, Ty::Variable(Variable::ExistentialVar(_))) => ()) |
rigid type parameter| Line | Coverage | Source |
|---|---|---|
| 160 | ✗ | (p in parameters.iter()) |
| 161 | ✗ | (may_contain_downstream_type(decls, env, assumptions, p) => ()) |
| ──────── ("rigid type parameter") | ||
| 163 | ✗ | (may_contain_downstream_type(decls, env, assumptions, RigidTy { name: _, parameters }) => ()) |
via normalize| Line | Coverage | Source |
|---|---|---|
| 169 | ✗ | (prove_normalize(decls, env, assumptions, parameter) => Constrained(p, c)) |
| 170 | N/A | (let assumptions = c.substitution().apply(assumptions)) |
| 171 | ✗ | (may_contain_downstream_type(decls, env, assumptions, p) => ()) |
| ──────── ("via normalize") | ||
| 173 | ✗ | (may_contain_downstream_type(decls, env, assumptions, parameter) => ()) |
forall| Line | Coverage | Source |
|---|---|---|
| 178 | ✗ | (scope(enter_existentially(env, binder) => (env, ty)) with() (may_contain_downstream_type(decls, env, assumptions, ty) => ())) |
| ──────── ("forall") | ||
| 181 | ✗ | (may_contain_downstream_type(decls, env, assumptions, Ty::PredicateTy(PredicateTy::ForAll(binder))) => ()) |