judgment_fn! {
fn prove_syntactically_eq(
_decls: Program,
env: Env,
assumptions: Predicates,
a: Parameter,
b: Parameter,
) => Constraints {
/* rules omitted */
}
}
Source: crates/formality-rust/src/prove/prove_normalize.rs:130
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 |
|---|
| 143 | 1 | (prove_syntactically_eq(decls, env, assumptions, b, a) => c) |
| | ──────── ("symmetric") |
| 145 | 1 | (prove_syntactically_eq(decls, env, assumptions, a, b) => c) |
rigid
| Line | Coverage | Source |
|---|
| 149 | N/A | (let RigidTy { name: a_name, parameters: a_parameters } = a) |
| 150 | N/A | (let RigidTy { name: b_name, parameters: b_parameters } = b) |
| 151 | ✗ | (if a_name == b_name) |
| 152 | ✗ | (zip(decls, env, assumptions, a_parameters.clone(), b_parameters.clone(), &prove_syntactically_eq) => c) |
| | ──────── ("rigid") |
| 154 | ✗ | (prove_syntactically_eq(decls, env, assumptions, Ty::RigidTy(a), Ty::RigidTy(b)) => c) |
alias
| Line | Coverage | Source |
|---|
| 158 | N/A | (let AliasTy { name: a_name, parameters: a_parameters } = a) |
| 159 | N/A | (let AliasTy { name: b_name, parameters: b_parameters } = b) |
| 160 | ✗ | (if a_name == b_name) |
| 161 | 1 | (zip(decls, env, assumptions, a_parameters.clone(), b_parameters.clone(), &prove_syntactically_eq) => c) |
| | ──────── ("alias") |
| 163 | 1 | (prove_syntactically_eq(decls, env, assumptions, Ty::AliasTy(a), Ty::AliasTy(b)) => c) |
existential-nonvar
| Line | Coverage | Source |
|---|
| 167 | 1 | (prove_existential_var_eq(decls, env, assumptions, v, t) => c) |
| | ──────── ("existential-nonvar") |
| 169 | 1 | (prove_syntactically_eq(decls, env, assumptions, Variable::ExistentialVar(v), t) => c) |
How to read this page