Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Negative coverage: check_crate / check crate / premise check_for_duplicate_items(program) => ()

Premise at line 70. Observed failure causes: inapplicable.

check crate
LineCoverageSource
706(check_for_duplicate_items(program) => ())
716(check_for_non_lifetime_binders(c) => ())
72✗(for_all(item in &c.items)
(check_crate_item(program, item, &c.id) => ()))
7411(check_coherence(program, c) => ())
──────── ("check crate")
76114(check_crate(program, Crate { id: _id, items: _items }) => ())

6 tests failed proving this premise:

Source location: tests/basic_tests.rs:328

#[test]
fn crate_with_duplicate_item_names() {
    FormalityTest::new(crates![crate core {
        struct A {}

        enum A {}
    }])
    .err(expect_test::expect![[r#"
            the rule "check crate" at (mod.rs) failed because
              the item name `A` is defined multiple times"#]]);

    FormalityTest::new(crates![crate core {
        trait a {}

        trait a {}
    }])
    .err(expect_test::expect![[r#"
            the rule "check crate" at (mod.rs) failed because
              the trait name `a` is defined multiple times"#]]);

    FormalityTest::new(crates![crate core {
        fn a() -> () { trusted }

        fn a() -> () { trusted }
    }])
    .err(expect_test::expect![[r#"
            the rule "check crate" at (mod.rs) failed because
              the function name `a` is defined multiple times"#]]);

    FormalityTest::new(crates![crate core {
        trait a {}

        fn a() -> () { trusted }
    }])
    .skip_execute()
    .ok();
}
Failed proof tree

Source location: tests/basic_tests.rs:337

#[test]
fn crate_with_duplicate_item_names() {
    FormalityTest::new(crates![crate core {
        struct A {}

        enum A {}
    }])
    .err(expect_test::expect![[r#"
            the rule "check crate" at (mod.rs) failed because
              the item name `A` is defined multiple times"#]]);

    FormalityTest::new(crates![crate core {
        trait a {}

        trait a {}
    }])
    .err(expect_test::expect![[r#"
            the rule "check crate" at (mod.rs) failed because
              the trait name `a` is defined multiple times"#]]);

    FormalityTest::new(crates![crate core {
        fn a() -> () { trusted }

        fn a() -> () { trusted }
    }])
    .err(expect_test::expect![[r#"
            the rule "check crate" at (mod.rs) failed because
              the function name `a` is defined multiple times"#]]);

    FormalityTest::new(crates![crate core {
        trait a {}

        fn a() -> () { trusted }
    }])
    .skip_execute()
    .ok();
}
Failed proof tree

Source location: tests/basic_tests.rs:346

fn a() -> () { trusted }
}])
(expect_test::expect![[r#"
    the rule "check crate" at (mod.rs) failed because
      the function name `a` is defined multiple times"#]]);

alityTest::new(crates![crate core {
trait a {}

fn a() -> () { trusted }
}])
p_execute()
);
}

#[test]
_impl_dup() {
alityTest::new(crates![crate core {
trait MyTrait {}
struct MyStruct {}
impl MyTrait for MyStruct {}
impl MyTrait for MyStruct {}
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
  `impl MyTrait for MyStruct { }` is defined multiple times"#]]);
}

#[test]
_neg_impl_dup() {
alityTest::new(crates![crate core {
trait MyTrait {}
struct MyStruct {}
impl !MyTrait for MyStruct {}
impl !MyTrait for MyStruct {}
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
  `impl ! MyTrait for MyStruct {}` is defined multiple times"#]]);
}

#[test]
missing_required_fn() {
alityTest::new(crates![crate core {
trait Foo {
    fn bar(self_: u32) -> u32;
}
Failed proof tree

Source location: tests/basic_tests.rs:367

#[test]
fn basic_impl_dup() {
    FormalityTest::new(crates![crate core {
        trait MyTrait {}
        struct MyStruct {}
        impl MyTrait for MyStruct {}
        impl MyTrait for MyStruct {}
    }])
    .err(expect_test::expect![[r#"
        the rule "check crate" at (mod.rs) failed because
          `impl MyTrait for MyStruct { }` is defined multiple times"#]]);
}
Failed proof tree

Source location: tests/basic_tests.rs:380

#[test]
fn basic_neg_impl_dup() {
    FormalityTest::new(crates![crate core {
        trait MyTrait {}
        struct MyStruct {}
        impl !MyTrait for MyStruct {}
        impl !MyTrait for MyStruct {}
    }])
    .err(expect_test::expect![[r#"
        the rule "check crate" at (mod.rs) failed because
          `impl ! MyTrait for MyStruct {}` is defined multiple times"#]]);
}
Failed proof tree

Source location: tests/coherence_overlap.rs:216

#[test]
fn u32_u32_impls() {
    FormalityTest::new(crates![crate core {
        trait Foo {}
        impl Foo for u32 {}
        impl Foo for u32 {}
    }])
    .err(expect_test::expect![[r#"
        the rule "check crate" at (mod.rs) failed because
          `impl Foo for u32 { }` is defined multiple times"#]])
}
Failed proof tree