Judgment check_fn
judgment_fn! {
/// Invoked for both free functions and methods.
///
/// * `env` -- the environment from the enclosing impl (if any)
/// * `assumptions` -- where-clauses from the enclosing impl (if any)
/// * `f` -- the function definition
pub(crate) fn check_fn(
program: Program,
env: Env,
assumptions: Predicates,
f: Fn,
crate_id: CrateId,
) => () {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/fns.rs:31
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.
check fn| Line | Coverage | Source |
|---|---|---|
| 48 | ✗ | (scope(enter_universally(env, &f.binder) => (env, FnBoundData { input_args, output_ty, where_clauses, body })) with() (let assumptions: Predicates = (assumptions, where_clauses).to_predicates()) (prove_where_clauses_well_formed(program, env, assumptions, where_clauses) => ()) (for_all(input_arg in input_args) (prove_goal(program, env, assumptions, AtomicPredicate::well_formed(&input_arg.ty)) => ())) (prove_goal(program, env, assumptions, AtomicPredicate::well_formed(output_ty)) => ()) (check_fn_body(program, env, assumptions, body, input_args, output_ty) => ())) |
| ──────── ("check fn") | ||
| 56 | 200 | (check_fn(program, env, assumptions, f, crate_id) => ()) |