Judgment check_fn at crates/formality-rust/src/check/fns.rs:31
Signature:
check_fn(program: Program, env: Env, assumptions: Wcs, f: Fn, crate_id: CrateId,) => ()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 | N/A | (let (env, bound_data) = env.instantiate_universally(&f.binder)) |
| 49 | N/A | (let FnBoundData { input_args, output_ty, where_clauses, body } = bound_data) |
| 50 | N/A | (let assumptions: Wcs = (assumptions, where_clauses).to_wcs()) |
| 51 | ✗ | (prove_where_clauses_well_formed(program, env, assumptions, where_clauses) => ()) |
| 52 | ✗ | (for_all(input_arg in input_args) (prove_goal(program, env, assumptions, Relation::well_formed(&input_arg.ty)) => ())) |
| 54 | ✗ | (prove_goal(program, env, assumptions, Relation::well_formed(output_ty)) => ()) |
| 55 | 46 | (check_fn_body(program, env, assumptions, body, input_args, output_ty) => ()) |
| ──────── ("check fn") | ||
| 57 | 81 | (check_fn(program, env, assumptions, f, crate_id) => ()) |