Parent tracking issue: #288
Convert check_neg_trait_impl from a regular Rust function to a judgment function.
Currently it: opens the binder, proves WF + not_implemented, and validates that negative impls are not declared unsafe.
See the parent tracking issue for context and examples.
This issue has been assigned to @Mslady-jojo via this comment.
Parent tracking issue: #288
Convert
check_neg_trait_implfrom a regular Rust function to a judgment function.Currently it: opens the binder, proves WF + not_implemented, and validates that negative impls are not declared unsafe.
See the parent tracking issue for context and examples.
This issue has been assigned to @Mslady-jojo via this comment.