judgment_fn! {
fn prove_normalize_via(
_decls: Program,
env: Env,
assumptions: Predicates,
via: Predicate,
goal: Parameter,
) => Constrained<Parameter> {
/* rules omitted */
}
}
Source: crates/formality-rust/src/prove/prove_normalize.rs:55
No applicable rule observed: at least one test exercised this judgment with no matching rule.
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.
var-axiom-l
| Line | Coverage | Source |
|---|
| 72 | ✗ | (if let Some(Variable::ExistentialVar(v_a)) = a.downcast()) |
| 73 | ✗ | (if v_goal == v_a) |
| | ──────── ("var-axiom-l") |
| 75 | ✗ | (prove_normalize_via(_decls, env, _assumptions, AtomicPredicate::Equals(a, b), Variable::ExistentialVar(v_goal)) => Constrained::none(env, b)) |
var-axiom-r
| Line | Coverage | Source |
|---|
| 79 | ✗ | (if let Some(Variable::ExistentialVar(v_a)) = a.downcast()) |
| 80 | ✗ | (if v_goal == v_a) |
| | ──────── ("var-axiom-r") |
| 82 | ✗ | (prove_normalize_via(_decls, env, _assumptions, AtomicPredicate::Equals(b, a), Variable::ExistentialVar(v_goal)) => Constrained::none(env, b)) |
axiom-l
| Line | Coverage | Source |
|---|
| 94 | ✗ | (if let None = goal.downcast::<ExistentialVar>()) |
| 95 | ✗ | (if goal != b) |
| 96 | 1 | (prove_syntactically_eq(decls, env, assumptions, a, goal) => c) |
| 97 | N/A | (let b = c.substitution().apply(b)) |
| | ──────── ("axiom-l") |
| 99 | 3 | (prove_normalize_via(decls, env, assumptions, AtomicPredicate::Equals(a, b), goal) => Constrained(b, c)) |
axiom-r
| Line | Coverage | Source |
|---|
| 103 | ✗ | (if let None = goal.downcast::<ExistentialVar>()) |
| 104 | ✗ | (if goal != b) |
| 105 | ✗ | (prove_syntactically_eq(decls, env, assumptions, a, goal) => c) |
| 106 | N/A | (let b = c.substitution().apply(b)) |
| | ──────── ("axiom-r") |
| 108 | 1 | (prove_normalize_via(decls, env, assumptions, AtomicPredicate::Equals(b, a), goal) => Constrained(b, c)) |
forall
| Line | Coverage | Source |
|---|
| 114 | ✗ | (scope(enter_existentially_with_constraints(env, binder) => (env, via1)) with(p, c)
(prove_normalize_via(decls, env, assumptions, via1, goal) => Constrained(p, c))) |
| | ──────── ("forall") |
| 117 | ✗ | (prove_normalize_via(decls, env, assumptions, Predicate::ForAll(binder), goal) => Constrained(p, c)) |
implies
| Line | Coverage | Source |
|---|
| 121 | ✗ | (prove_normalize_via(decls, env, assumptions, wc_consequence, goal) => Constrained(p, c)) |
| 122 | ✗ | (prove_after(decls, c, assumptions, wc_condition) => c) |
| 123 | N/A | (let p = c.substitution().apply(p)) |
| | ──────── ("implies") |
| 125 | ✗ | (prove_normalize_via(decls, env, assumptions, Predicate::Implies(wc_condition, wc_consequence), goal) => Constrained(p, c)) |
How to read this page