Signature:
prove_via(_decls: Program, env: Env, assumptions: Wcs, via: WcData, goal: WcData,) => Constraints
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.
predicate-congruence-axiom
| Line | Coverage | Source |
|---|
| 27 | N/A | (let (skel_c, parameters_c) = pred_1.debone()) |
| 29 | N/A | (let (skel_g, parameters_g) = pred_2.debone()) |
| 30 | ✗ | (if skel_c == skel_g) |
| 31 | 2 | (prove(decls, env, assumptions, Wcs::all_eq(parameters_c, parameters_g)) => c) |
| | ──────── ("predicate-congruence-axiom") |
| 33 | 13 | (prove_via(decls, env, assumptions, WcData::Predicate(pred_1), WcData::Predicate(pred_2)) => c) |
relation-axiom
| Line | Coverage | Source |
|---|
| 37 | N/A | (let (skel_c, parameters_c) = rel_1.debone()) |
| 38 | N/A | (let (skel_g, parameters_g) = rel_2.debone()) |
| 39 | ✗ | (if skel_c == skel_g) |
| 40 | ✗ | (if parameters_c == parameters_g) |
| | ──────── ("relation-axiom") |
| 42 | 4 | (prove_via(_decls, env, _assumptions, WcData::Relation(rel_1), WcData::Relation(rel_2)) => Constraints::none(env)) |
forall
| Line | Coverage | Source |
|---|
| 47 | N/A | (let (env, subst) = env.existential_substitution(binder)) |
| 48 | N/A | (let via1 = binder.instantiate_with(&subst).unwrap()) |
| 50 | 1 | (prove_via(decls, env, assumptions, via1, goal) => c) |
| | ──────── ("forall") |
| 52 | 2 | (prove_via(decls, env, assumptions, WcData::ForAll(binder), goal) => c.pop_subst(&subst)) |
implies
| Line | Coverage | Source |
|---|
| 58 | ✗ | (prove_via(decls, env, assumptions, wc_consequence, goal) => c) |
| 60 | ✗ | (prove_after(decls, c, assumptions, wc_condition) => c) |
| | ──────── ("implies") |
| 62 | ✗ | (prove_via(decls, env, assumptions, WcData::Implies(wc_condition, wc_consequence), goal) => c) |