Signature:
prove_sub(_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.
normalize-l
| Line | Coverage | Source |
|---|
| 28 | 5 | (prove_normalize(decls, env, assumptions, x) => Constrained(y, c)) |
| 29 | ✗ | (prove_after(decls, c, assumptions, Relation::sub(y, z)) => c) |
| | ──────── ("normalize-l") |
| 31 | 16 | (prove_sub(decls, env, assumptions, x, z) => c) |
normalize-r
| Line | Coverage | Source |
|---|
| 35 | 5 | (prove_normalize(decls, env, assumptions, y) => Constrained(z, c)) |
| 36 | ✗ | (prove_after(decls, c, assumptions, Relation::sub(x, &z)) => c) |
| | ──────── ("normalize-r") |
| 38 | 2 | (prove_sub(decls, env, assumptions, x, y) => c) |
rigid
| Line | Coverage | Source |
|---|
| 42 | N/A | (let RigidTy { name: a_name, parameters: a_parameters } = a) |
| 43 | N/A | (let RigidTy { name: b_name, parameters: b_parameters } = b) |
| 44 | ✗ | (if a_name == b_name) |
| 45 | ✗ | (prove(decls, env, assumptions, Wcs::all_sub(a_parameters, b_parameters)) => c) |
| | ──────── ("rigid") |
| 47 | 19 | (prove_sub(decls, env, assumptions, TyData::RigidTy(a), TyData::RigidTy(b)) => c) |
lifetime => outlives
| Line | Coverage | Source |
|---|
| 51 | ✗ | (prove_outlives(decls, env, assumptions, a, b) => c) |
| | ──────── ("lifetime => outlives") |
| 53 | 18 | (prove_sub(decls, env, assumptions, a: Lt, b: Lt) => c) |