Judgment prove_after
judgment_fn! {
pub fn prove_after(
_decls: Program,
constraints: Constraints,
assumptions: Predicates,
goal: Predicates,
) => Constraints {
/* rules omitted */
}
}Source: crates/formality-rust/src/prove/prove_after.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.
prove_after| Line | Coverage | Source |
|---|---|---|
| 18 | N/A | (let (assumptions, goal) = c1.substitution().apply((assumptions, goal))) |
| 19 | 21 | (prove(decls, c1.env(), assumptions, goal) => c2) |
| ──────── ("prove_after") | ||
| 21 | 237 | (prove_after(decls, c1, assumptions, goal) => c1.seq(c2)) |