Judgment check_neg_trait_impl
judgment_fn! {
pub(super) fn check_neg_trait_impl(
program: Program,
trait_impl: NegTraitImpl,
) => () {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/impls.rs:46
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_neg_trait_impl| Line | Coverage | Source |
|---|---|---|
| 54 | 2 | (fail "negative impls cannot be unsafe") |
| ──────── ("check_neg_trait_impl") | ||
| 56 | 3 | (check_neg_trait_impl(program, NegTraitImpl { binder: _, safety: Safety::Unsafe }) => ()) |
check_neg_trait_impl| Line | Coverage | Source |
|---|---|---|
| 60 | ✗ | (scope(enter_universally(Env::default(), binder) => (env, NegTraitImplBoundData { trait_id, self_ty, trait_parameters, where_clauses })) with() (let trait_ref = trait_id.with(self_ty, trait_parameters)) (super::where_clauses::prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ()) (super::prove_goal(program, env, where_clauses, AtomicPredicate::not_implemented(&trait_ref)) => ()) (let trait_decl = program.program().trait_named(&trait_ref.trait_id)?) (let TraitBoundData { where_clauses: _, trait_items: _ } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?)) |
| ──────── ("check_neg_trait_impl") | ||
| 69 | 3 | (check_neg_trait_impl(program, NegTraitImpl { binder, safety: Safety::Safe }) => ()) |