judgment_fn! {
pub fn prove_eq(
_decls: Program,
env: Env,
assumptions: Predicates,
a: Parameter,
b: Parameter,
) => Constraints {
/* rules omitted */
}
}
Source: crates/formality-rust/src/prove/prove_eq.rs:23
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.
symmetric
| Line | Coverage | Source |
|---|
| 38 | 17 | (prove_eq(decls, env, assumptions, r, l) => env_c) |
| | ──────── ("symmetric") |
| 40 | 220 | (prove_eq(decls, env, assumptions, l, r) => env_c) |
rigid
| Line | Coverage | Source |
|---|
| 44 | N/A | (let RigidTy { name: a_name, parameters: a_parameters } = a) |
| 45 | N/A | (let RigidTy { name: b_name, parameters: b_parameters } = b) |
| 46 | ✗ | (if a_name == b_name) |
| 47 | 1 | (prove(decls, env, assumptions, Predicates::all_eq(a_parameters, b_parameters)) => c) |
| | ──────── ("rigid") |
| 49 | 201 | (prove_eq(decls, env, assumptions, Ty::RigidTy(a), Ty::RigidTy(b)) => c) |
alias
| Line | Coverage | Source |
|---|
| 53 | N/A | (let AliasTy { name: a_name, parameters: a_parameters } = a) |
| 54 | N/A | (let AliasTy { name: b_name, parameters: b_parameters } = b) |
| 55 | ✗ | (if a_name == b_name) |
| 56 | 1 | (prove(decls, env, assumptions, Predicates::all_eq(a_parameters, b_parameters)) => env_c) |
| | ──────── ("alias") |
| 58 | 1 | (prove_eq(decls, env, assumptions, Ty::AliasTy(a), Ty::AliasTy(b)) => env_c) |
existential
| Line | Coverage | Source |
|---|
| 62 | 5 | (prove_existential_var_eq(decls, env, assumptions, v, r) => c) |
| | ──────── ("existential") |
| 64 | 223 | (prove_eq(decls, env, assumptions, Variable::ExistentialVar(v), r) => c) |
normalize-l
| Line | Coverage | Source |
|---|
| 68 | 17 | (prove_normalize(decls, env, assumptions, x) => Constrained(y, c)) |
| 69 | 3 | (prove_after(decls, c, assumptions, eq(y, z)) => c) |
| | ──────── ("normalize-l") |
| 71 | 26 | (prove_eq(decls, env, assumptions, x, z) => c) |
How to read this page