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: prove_wc / positive impl / premise prove_after(decls, c, co_assumptions, &i.where_clause) => c

Premise at line 80. Observed failure causes: failed_judgment.

positive impl
LineCoverageSource
63✗(i in decls.impl_decls(&trait_ref.trait_id))
66N/A(let (env, subst) = env.existential_substitution(&i.binder))
67N/A(let i = i.binder.instantiate_with(&subst).unwrap())
71N/A(let t = decls.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap())
78N/A(let co_assumptions = (assumptions, trait_ref))
797(prove(decls, env, co_assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
802(prove_after(decls, c, co_assumptions, &i.where_clause) => c)
864(prove_after(decls, c, assumptions, &t.where_clause) => c)
──────── ("positive impl")
88153(prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))

2 tests failed proving this premise:

Source location: tests/drop.rs:132

#[test]
fn drop_impl_extra_where_clause() {
    FormalityTest::new(crates![
        crate Foo {
            trait Clone {}

            struct MyStruct<T> {
                value: T,
            }

            impl<T> Drop for MyStruct<T> where T: Clone {}
        }
    ])
    .err(expect_test::expect![[r#"
        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: Clone(!ty_0), via: Drop(MyStruct<!ty_0>), assumptions: {Drop(MyStruct<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "trait implied bound" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.trait_invariants()`

        the rule "trait implied bound" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.trait_invariants()`"#]])
}
Failed proof tree

Source location: tests/drop.rs:191

#[test]
fn drop_impl_enum_extra_where_clause() {
    FormalityTest::new(crates![
        crate Foo {
            trait Clone {}

            enum MyEnum<T> {
                Value{value: T},
            }

            impl<T> Drop for MyEnum<T> where T: Clone {}
        }
    ])
    .err(expect_test::expect![[r#"
        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: Clone(!ty_0), via: Drop(MyEnum<!ty_0>), assumptions: {Drop(MyEnum<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "trait implied bound" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.trait_invariants()`

        the rule "trait implied bound" at (prove_wc.rs) failed because
          expression evaluated to an empty collection: `decls.trait_invariants()`"#]])
}
Failed proof tree