Judgment prove_predicate_list
judgment_fn! {
/// Prove that all elements in `goals`, a list of where-clauses, are true, one after the other.
pub fn prove_predicate_list(
_decls: Program,
env: Env,
assumptions: Predicates,
goals: Predicates,
) => Constraints {
/* rules omitted */
}
}Source: crates/formality-rust/src/prove/prove_predicate_list.rs:8
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.
none| Line | Coverage | Source |
|---|---|---|
| ──────── ("none") | ||
| 22 | 238 | (prove_predicate_list(_decls, env, _assumptions, ()) => Constraints::none(env)) |
some| Line | Coverage | Source |
|---|---|---|
| 26 | 67 | (prove_predicate(decls, env, assumptions, wc0) => c) |
| 27 | 2 | (prove_after(decls, c, assumptions, wcs1) => c) |
| ──────── ("some") | ||
| 29 | 237 | (prove_predicate_list(decls, env, assumptions, Cons(wc0, wcs1)) => c) |