Judgment is_local_trait_ref
judgment_fn! {
pub fn is_local_trait_ref(
_decls: Program,
env: Env,
assumptions: Predicates,
goal: TraitRef,
) => Constraints {
/* rules omitted */
}
}Source: crates/formality-rust/src/prove/is_local.rs:206
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.
local trait| Line | Coverage | Source |
|---|---|---|
| 216 | 12 | (if decls.is_local_trait_id(&goal.trait_id)) |
| ──────── ("local trait") | ||
| 218 | 205 | (is_local_trait_ref(decls, env, _assumptions, goal) => Constraints::none(env)) |
local parameter| Line | Coverage | Source |
|---|---|---|
| 223 | ✗ | (i in 0 .. goal.parameters.len()) |
| 224 | 12 | (is_local_parameter(decls, env, assumptions, &goal.parameters[*i]) => c1) |
| 227 | N/A | (let assumptions = c1.substitution().apply(assumptions)) |
| 228 | N/A | (let goal = c1.substitution().apply(goal)) |
| 229 | 4 | (for_all(decls, env, assumptions, &goal.parameters[..*i], &is_not_downstream) => c2) |
| ──────── ("local parameter") | ||
| 231 | 14 | (is_local_trait_ref(decls, env, assumptions, goal) => c1.seq(c2)) |