Judgment normalizes_to_not_downstream
judgment_fn! {
fn normalizes_to_not_downstream(
_decls: Program,
env: Env,
assumptions: Predicates,
parameter: Parameter,
) => Constraints {
/* rules omitted */
}
}Source: crates/formality-rust/src/prove/is_local.rs:187
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.
ambiguous| Line | Coverage | Source |
|---|---|---|
| 197 | ✗ | (prove_normalize(decls, env, assumptions, parameter) => Constrained(parameter, c1)) |
| 198 | N/A | (let assumptions = c1.substitution().apply(assumptions)) |
| 199 | ✗ | (is_not_downstream(decls, env, assumptions, parameter) => c2) |
| ──────── ("ambiguous") | ||
| 201 | ✗ | (normalizes_to_not_downstream(decls, env, assumptions, parameter) => c1.seq(c2)) |