Signature:
prove_syntactically_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 |
|---|
| 146 | 1 | (prove_syntactically_eq(decls, env, assumptions, b, a) => c) |
| | ──────── ("symmetric") |
| 148 | 1 | (prove_syntactically_eq(decls, env, assumptions, a, b) => c) |
rigid
| Line | Coverage | Source |
|---|
| 152 | N/A | (let RigidTy { name: a_name, parameters: a_parameters } = a) |
| 153 | N/A | (let RigidTy { name: b_name, parameters: b_parameters } = b) |
| 154 | ✗ | (if a_name == b_name) |
| 155 | ✗ | (zip(decls, env, assumptions, a_parameters.clone(), b_parameters.clone(), &prove_syntactically_eq) => c) |
| | ──────── ("rigid") |
| 157 | ✗ | (prove_syntactically_eq(decls, env, assumptions, TyData::RigidTy(a), TyData::RigidTy(b)) => c) |
alias
| Line | Coverage | Source |
|---|
| 161 | N/A | (let AliasTy { name: a_name, parameters: a_parameters } = a) |
| 162 | N/A | (let AliasTy { name: b_name, parameters: b_parameters } = b) |
| 163 | ✗ | (if a_name == b_name) |
| 164 | 1 | (zip(decls, env, assumptions, a_parameters.clone(), b_parameters.clone(), &prove_syntactically_eq) => c) |
| | ──────── ("alias") |
| 166 | 1 | (prove_syntactically_eq(decls, env, assumptions, TyData::AliasTy(a), TyData::AliasTy(b)) => c) |
existential-nonvar
| Line | Coverage | Source |
|---|
| 170 | 1 | (prove_existential_var_eq(decls, env, assumptions, v, t) => c) |
| | ──────── ("existential-nonvar") |
| 172 | 1 | (prove_syntactically_eq(decls, env, assumptions, Variable::ExistentialVar(v), t) => c) |