Judgment check_adt at crates/formality-rust/src/check/adts.rs:11
Signature:
check_adt(program: Program, adt: Adt,) => ()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 adt| Line | Coverage | Source |
|---|---|---|
| 18 | 2 | (check_adt_variant_names_unique(adt) => ()) |
| 19 | N/A | (let (env, bound_data) = Env::default().instantiate_universally(&adt.binder)) |
| 20 | N/A | (let AdtBoundData { where_clauses, variants } = bound_data) |
| 21 | 1 | (prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ()) |
| 22 | ✗ | (for_all(variant in variants) (let Variant { fields, .. } = variant) (for_all(field in fields) (let Field { ty, .. } = field) (prove_goal(program, env, where_clauses, Relation::well_formed(ty)) => ()))) |
| ──────── ("check adt") | ||
| 28 | 31 | (check_adt(program, adt) => ()) |