Judgment prove_via
judgment_fn! {
/// Check whether the where-clause `via` (which is one of the `assumptions` that are in in scope)
/// can be used to prove `goal` (the thing we are trying to prove).
///
/// This is equivalent to the "elaboration" of the environment that takes place in rustc,
/// but done lazilly. For example, if you have `where T: Eq` then you can clearly prove `T: Eq`
/// but you can also prove `T: PartialEq` because `trait Eq: PartialEq`.
pub fn prove_via(
_decls: Program,
env: Env,
assumptions: Predicates,
via: Predicate,
goal: Predicate,
) => Constraints {
/* rules omitted */
}
}Source: crates/formality-rust/src/prove/prove_via.rs:9
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.is_relation()) |
| 31 | ✗ | (if skel_c == skel_g) |
| 32 | 2 | (prove(decls, env, assumptions, Predicates::all_eq(parameters_c, parameters_g)) => c) |
| ──────── ("predicate-congruence-axiom") | ||
| 34 | 16 | (prove_via(decls, env, assumptions, Predicate::AtomicPredicate(pred_1), Predicate::AtomicPredicate(pred_2)) => c) |
relation-axiom| Line | Coverage | Source |
|---|---|---|
| 38 | N/A | (let (skel_c, parameters_c) = rel_1.debone()) |
| 39 | N/A | (let (skel_g, parameters_g) = rel_2.debone()) |
| 40 | ✗ | (if skel_c.is_relation()) |
| 41 | ✗ | (if skel_c == skel_g) |
| 42 | ✗ | (if parameters_c == parameters_g) |
| ──────── ("relation-axiom") | ||
| 44 | 8 | (prove_via(_decls, env, _assumptions, Predicate::AtomicPredicate(rel_1), Predicate::AtomicPredicate(rel_2)) => Constraints::none(env)) |
forall| Line | Coverage | Source |
|---|---|---|
| 49 | ✗ | (scope(enter_existentially_with_constraints(env, binder) => (env, via1)) with(c) // Try to prove `T: Trait<?a> == goal`. (prove_via(decls, env, assumptions, via1, goal) => c)) |
| ──────── ("forall") | ||
| 53 | 2 | (prove_via(decls, env, assumptions, Predicate::ForAll(binder), goal) => c) |
implies| Line | Coverage | Source |
|---|---|---|
| 59 | ✗ | (prove_via(decls, env, assumptions, wc_consequence, goal) => c) |
| 61 | ✗ | (prove_after(decls, c, assumptions, wc_condition) => c) |
| ──────── ("implies") | ||
| 63 | ✗ | (prove_via(decls, env, assumptions, Predicate::Implies(wc_condition, wc_consequence), goal) => c) |