Signature:
prove_eq(_decls: Program, env: Env, assumptions: Wcs, a: Parameter, b: Parameter,) => Constraints
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 | 15 | (prove_eq(decls, env, assumptions, r, l) => env_c) |
| | ──────── ("symmetric") |
| 40 | 155 | (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, Wcs::all_eq(a_parameters, b_parameters)) => c) |
| | ──────── ("rigid") |
| 49 | 136 | (prove_eq(decls, env, assumptions, TyData::RigidTy(a), TyData::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, Wcs::all_eq(a_parameters, b_parameters)) => env_c) |
| | ──────── ("alias") |
| 58 | 1 | (prove_eq(decls, env, assumptions, TyData::AliasTy(a), TyData::AliasTy(b)) => env_c) |
existential
| Line | Coverage | Source |
|---|
| 62 | 5 | (prove_existential_var_eq(decls, env, assumptions, v, r) => c) |
| | ──────── ("existential") |
| 64 | 158 | (prove_eq(decls, env, assumptions, Variable::ExistentialVar(v), r) => c) |
normalize-l
| Line | Coverage | Source |
|---|
| 68 | 15 | (prove_normalize(decls, env, assumptions, x) => Constrained(y, c)) |
| 69 | 3 | (prove_after(decls, c, assumptions, eq(y, z)) => c) |
| | ──────── ("normalize-l") |
| 71 | 18 | (prove_eq(decls, env, assumptions, x, z) => c) |