judgment_fn! {
pub fn prove_sub(
_decls: Program,
env: Env,
assumptions: Predicates,
a: Parameter,
b: Parameter,
) => Constraints {
/* rules omitted */
}
}
Source: crates/formality-rust/src/prove/prove_sub.rs:12
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.
normalize-l
| Line | Coverage | Source |
|---|
| 27 | 11 | (prove_normalize(decls, env, assumptions, x) => Constrained(y, c)) |
| 28 | ✗ | (prove_after(decls, c, assumptions, AtomicPredicate::sub(y, z)) => c) |
| | ──────── ("normalize-l") |
| 30 | 29 | (prove_sub(decls, env, assumptions, x, z) => c) |
normalize-r
| Line | Coverage | Source |
|---|
| 34 | 11 | (prove_normalize(decls, env, assumptions, y) => Constrained(z, c)) |
| 35 | ✗ | (prove_after(decls, c, assumptions, AtomicPredicate::sub(x, &z)) => c) |
| | ──────── ("normalize-r") |
| 37 | 12 | (prove_sub(decls, env, assumptions, x, y) => c) |
rigid
| Line | Coverage | Source |
|---|
| 41 | N/A | (let RigidTy { name: a_name, parameters: a_parameters } = a) |
| 42 | N/A | (let RigidTy { name: b_name, parameters: b_parameters } = b) |
| 43 | ✗ | (if a_name == b_name) |
| 44 | ✗ | (prove(decls, env, assumptions, Predicates::all_sub(a_parameters, b_parameters)) => c) |
| | ──────── ("rigid") |
| 46 | 33 | (prove_sub(decls, env, assumptions, Ty::RigidTy(a), Ty::RigidTy(b)) => c) |
lifetime => outlives
| Line | Coverage | Source |
|---|
| 50 | ✗ | (prove_outlives(decls, env, assumptions, a, b) => c) |
| | ──────── ("lifetime => outlives") |
| 52 | 29 | (prove_sub(decls, env, assumptions, a: Lt, b: Lt) => c) |
How to read this page