Judgment prove_const_has_type
judgment_fn! {
/// The "heart" of the trait system -- prove that a where-clause holds given a set of declarations, variable environment, and set of assumptions.
/// If successful, returns the constraints under which the where-clause holds.
pub fn prove_const_has_type(
decls: Program,
env: Env,
assumptions: Predicates,
constant: Const,
) => (Ty, Constraints) {
/* rules omitted */
}
}Source: crates/formality-rust/src/prove/prove_const_has_type.rs:11
No applicable rule observed: at least one test exercised this judgment with no matching rule.
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.
rigid constant| Line | Coverage | Source |
|---|---|---|
| ──────── ("rigid constant") | ||
| 29 | 4 | (prove_const_has_type(_decls, env, _assumptions, Const::Scalar(scalar)) => (scalar.ty(), Constraints::none(env))) |
block| Line | Coverage | Source |
|---|---|---|
| 34 | ✗ | (borrow_check(TypeckEnv::for_const(env, decls), assumptions, FlowState::default(), block) => ()) |
| ──────── ("block") | ||
| 36 | ✗ | (prove_const_has_type(decls, env, assumptions, Const::Block(block)) => (Ty::unit(), Constraints::none(env))) |