Negative coverage: check_adt / check adt / premise check_adt_variant_names_unique(adt) => ()
Premise at line 18. Observed failure causes: inapplicable.
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) => ()) |
2 tests failed proving this premise:
Source location: tests/basic_tests.rs:277
#[test]
fn basic_adt_variant_dup() {
FormalityTest::new(crates![crate Foo {
enum Bar {
Baz{},
Baz{},
}
}])
.err(expect_test::expect![[r#"
the rule "check adt" at (adts.rs) failed because
variant "Baz" defined multiple times"#]])
}Failed proof tree
check_all_crates failedmod.rs:41rule "check all prefixes"mod.rs:53check_crate failedmod.rs:60rule "check crate"mod.rs:73check_crate_item failedmod.rs:163rule "adt"mod.rs:185check_adt failedadts.rs:11rule "check adt"adts.rs:18 (failed: inapplicable)
Source location: tests/basic_tests.rs:290
#[test]
fn basic_adt_field_dup() {
FormalityTest::new(crates![crate Foo {
struct Bar {
baz: (),
baz: (),
}
}])
.err(expect_test::expect![[r#"
the rule "check adt" at (adts.rs) failed because
field "baz" of variant "struct" defined multiple times"#]])
}Failed proof tree
check_all_crates failedmod.rs:41rule "check all prefixes"mod.rs:53check_crate failedmod.rs:60rule "check crate"mod.rs:73check_crate_item failedmod.rs:163rule "adt"mod.rs:185check_adt failedadts.rs:11rule "check adt"adts.rs:18 (failed: inapplicable)