Judgment may_be_downstream_parameter
judgment_fn! {
fn may_be_downstream_parameter(
_decls: Program,
env: Env,
assumptions: Predicates,
parameter: Parameter,
) => Constraints {
/* rules omitted */
}
}Source: crates/formality-rust/src/prove/is_local.rs:94
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.
type variable| Line | Coverage | Source |
|---|---|---|
| ──────── ("type variable") | ||
| 107 | ✗ | (may_be_downstream_parameter(_decls, env, _assumptions, Ty::Variable(Variable::ExistentialVar(_))) => Constraints::none(env)) |
via normalize| Line | Coverage | Source |
|---|---|---|
| 119 | ✗ | (p in parameters.iter()) |
| 120 | ✗ | (may_contain_downstream_type(decls, env, assumptions, p) => ()) |
| 123 | ✗ | (may_not_be_provable(env, assumptions, &AliasTy::new(name, parameters), |env, assumptions, alias| normalizes_to_not_downstream(decls, &env, &assumptions, &alias) ) => c) |
| ──────── ("via normalize") | ||
| 127 | ✗ | (may_be_downstream_parameter(decls, env, assumptions, AliasTy { name, parameters }) => c) |
fundamental rigid type| Line | Coverage | Source |
|---|---|---|
| 132 | ✗ | (if is_fundamental(decls, name)) |
| 133 | ✗ | (p in parameters.iter()) |
| 134 | ✗ | (may_be_downstream_parameter(decls, env, assumptions, p) => c) |
| ──────── ("fundamental rigid type") | ||
| 136 | ✗ | (may_be_downstream_parameter(decls, env, assumptions, RigidTy { name, parameters }) => c) |