Skip to content

clippy reports unused imports when using both requires and ensures #9

Activity

robjtede

robjtede commented on May 2, 2025

@robjtede
MemberAuthor

The thing about this one is that any combination of attributes are inextricably linked because the code they generate is not strictly additive. Each attribute does a scan for the other attributes.

Making this more intitive for users would require a change of syntax that uses a single attribute. E.g.,

#[contract(
  requires( n != T::zero() || d != T::zero() )],
  ensures( ret != T::zero() && n % ret == T::zero() && d % ret == T::zero()),
)]
pub fn euclidean<T>(n: T, d: T) -> T
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

      Development

      No branches or pull requests

        Participants

        @robjtede

        Issue actions

          clippy reports unused imports when using both requires and ensures · Issue #9 · x52dev/contracts