Judgment check_adt
judgment_fn! {
pub(super) fn check_adt(
program: Program,
adt: Adt,
) => () {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/adts.rs:11
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 | ✗ | (scope(enter_universally(Env::default(), &adt.binder) => (env, AdtBoundData { where_clauses, variants })) with() (prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ()) (for_all(variant in variants) (let Variant { fields, .. } = variant) (for_all(field in fields) (let Field { ty, .. } = field) (prove_goal(program, env, where_clauses, AtomicPredicate::well_formed(ty)) => ())))) |
| ──────── ("check adt") | ||
| 27 | 59 | (check_adt(program, adt) => ()) |