judgment_fn! {
fn is_local_parameter(
_decls: Program,
env: Env,
assumptions: Predicates,
goal: Parameter,
) => Constraints {
/* rules omitted */
}
}
Source: crates/formality-rust/src/prove/is_local.rs:293
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 parameter
| Line | Coverage | Source |
|---|
| 305 | 12 | (prove_normalize(decls, env, assumptions, goal) => Constrained(p, c1)) |
| 306 | N/A | (let assumptions = c1.substitution().apply(assumptions)) |
| 307 | 2 | (is_local_parameter(decls, c1.env(), assumptions, p) => c2) |
| | ──────── ("local parameter") |
| 309 | 1 | (is_local_parameter(decls, env, assumptions, goal) => c1.seq(c2)) |
fundamental rigid type
| Line | Coverage | Source |
|---|
| 314 | 7 | (if is_fundamental(decls, name)) |
| 315 | N/A | (let type_params: Vec<Parameter> = parameters.iter().filter(|p| !matches!(p, Parameter::Lt(_))).cloned().collect()) |
| 316 | 5 | (for_all(decls, env, assumptions, type_params, &is_local_parameter) => c) |
| | ──────── ("fundamental rigid type") |
| 318 | 2 | (is_local_parameter(decls, env, assumptions, RigidTy { name, parameters }) => c) |
local rigid type
| Line | Coverage | Source |
|---|
| 323 | 5 | (if decls.is_local_adt_id(a)) |
| | ──────── ("local rigid type") |
| 325 | 13 | (is_local_parameter(decls, env, _assumptions, RigidTy { name: RigidName::AdtId(a), parameters: _ }) => Constraints::none(env)) |
existential variable
| Line | Coverage | Source |
|---|
| | ──────── ("existential variable") |
| 331 | 1 | (is_local_parameter(_decls, env, _assumptions, Ty::Variable(Variable::ExistentialVar(_))) => Constraints::none(env).ambiguous()) |
How to read this page