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 |
|---|
| 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, Relation::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, Relation::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, Relation::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 | ✗ | (prove_normalize_via(decls, env, assumptions, Relation::Equals(b, a), goal) => Constrained(b, c)) |
forall
| Line | Coverage | Source |
|---|
| 114 | N/A | (let (env, subst) = env.existential_substitution(binder)) |
| 115 | N/A | (let via1 = binder.instantiate_with(&subst).unwrap()) |
| 116 | ✗ | (prove_normalize_via(decls, env, assumptions, via1, goal) => Constrained(p, c)) |
| 117 | N/A | (let c = c.pop_subst(&subst)) |
| 118 | ✗ | (assert c.env().encloses(&p)) |
| | ──────── ("forall") |
| 120 | ✗ | (prove_normalize_via(decls, env, assumptions, WcData::ForAll(binder), goal) => Constrained(p, c)) |
implies
| Line | Coverage | Source |
|---|
| 124 | ✗ | (prove_normalize_via(decls, env, assumptions, wc_consequence, goal) => Constrained(p, c)) |
| 125 | ✗ | (prove_after(decls, c, assumptions, wc_condition) => c) |
| 126 | N/A | (let p = c.substitution().apply(p)) |
| | ──────── ("implies") |
| 128 | ✗ | (prove_normalize_via(decls, env, assumptions, WcData::Implies(wc_condition, wc_consequence), goal) => Constrained(p, c)) |