Signature:
prove_normalize_via(_decls: Program, env: Env, assumptions: Wcs, via: Wc, goal: Parameter,) => Constrained<Parameter>
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 |
|---|
| 71 | ✗ | (if let Some(Variable::ExistentialVar(v_a)) = a.downcast()) |
| 72 | ✗ | (if v_goal == v_a) |
| | ──────── ("var-axiom-l") |
| 74 | ✗ | (prove_normalize_via(_decls, env, _assumptions, Predicate::Equals(a, b), Variable::ExistentialVar(v_goal)) => Constrained::none(env, b)) |
var-axiom-r
| Line | Coverage | Source |
|---|
| 78 | ✗ | (if let Some(Variable::ExistentialVar(v_a)) = a.downcast()) |
| 79 | ✗ | (if v_goal == v_a) |
| | ──────── ("var-axiom-r") |
| 81 | ✗ | (prove_normalize_via(_decls, env, _assumptions, Predicate::Equals(b, a), Variable::ExistentialVar(v_goal)) => Constrained::none(env, b)) |
axiom-l
| Line | Coverage | Source |
|---|
| 93 | ✗ | (if let None = goal.downcast::<ExistentialVar>()) |
| 94 | ✗ | (if goal != b) |
| 95 | 1 | (prove_syntactically_eq(decls, env, assumptions, a, goal) => c) |
| 96 | N/A | (let b = c.substitution().apply(b)) |
| | ──────── ("axiom-l") |
| 98 | 3 | (prove_normalize_via(decls, env, assumptions, Predicate::Equals(a, b), goal) => Constrained(b, c)) |
axiom-r
| Line | Coverage | Source |
|---|
| 102 | ✗ | (if let None = goal.downcast::<ExistentialVar>()) |
| 103 | ✗ | (if goal != b) |
| 104 | ✗ | (prove_syntactically_eq(decls, env, assumptions, a, goal) => c) |
| 105 | N/A | (let b = c.substitution().apply(b)) |
| | ──────── ("axiom-r") |
| 107 | ✗ | (prove_normalize_via(decls, env, assumptions, Predicate::Equals(b, a), goal) => Constrained(b, c)) |
forall
| Line | Coverage | Source |
|---|
| 113 | N/A | (let (env, subst) = env.existential_substitution(binder)) |
| 114 | N/A | (let via1 = binder.instantiate_with(&subst).unwrap()) |
| 115 | ✗ | (prove_normalize_via(decls, env, assumptions, via1, goal) => Constrained(p, c)) |
| 116 | N/A | (let c = c.pop_subst(&subst)) |
| 117 | ✗ | (assert c.env().encloses(&p)) |
| | ──────── ("forall") |
| 119 | ✗ | (prove_normalize_via(decls, env, assumptions, Wc::ForAll(binder), goal) => Constrained(p, c)) |
implies
| Line | Coverage | Source |
|---|
| 123 | ✗ | (prove_normalize_via(decls, env, assumptions, wc_consequence, goal) => Constrained(p, c)) |
| 124 | ✗ | (prove_after(decls, c, assumptions, wc_condition) => c) |
| 125 | N/A | (let p = c.substitution().apply(p)) |
| | ──────── ("implies") |
| 127 | ✗ | (prove_normalize_via(decls, env, assumptions, Wc::Implies(wc_condition, wc_consequence), goal) => Constrained(p, c)) |