Judgment is_local_trait_ref at crates/formality-rust/src/prove/prove/prove/is_local.rs:201
Signature:
is_local_trait_ref(_decls: Program, env: Env, assumptions: Wcs, goal: TraitRef,) => ConstraintsThe number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.
local trait| Line | Coverage | Source |
|---|---|---|
| 211 | 6 | (if decls.is_local_trait_id(&goal.trait_id)) |
| ──────── ("local trait") | ||
| 213 | 109 | (is_local_trait_ref(decls, env, _assumptions, goal) => Constraints::none(env)) |
local parameter| Line | Coverage | Source |
|---|---|---|
| 218 | ✗ | (i in 0 .. goal.parameters.len()) |
| 219 | 6 | (is_local_parameter(decls, env, assumptions, &goal.parameters[*i]) => c1) |
| 222 | N/A | (let assumptions = c1.substitution().apply(assumptions)) |
| 223 | N/A | (let goal = c1.substitution().apply(goal)) |
| 224 | 1 | (for_all(decls, env, assumptions, &goal.parameters[..*i], &is_not_downstream) => c2) |
| ──────── ("local parameter") | ||
| 226 | 9 | (is_local_trait_ref(decls, env, assumptions, goal) => c1.seq(c2)) |