Skip to content

Remove unneeded discrete and indiscrete traits#1675

Merged
prabau merged 1 commit intomainfrom
discrete-indiscrete-cleanup
Mar 13, 2026
Merged

Remove unneeded discrete and indiscrete traits#1675
prabau merged 1 commit intomainfrom
discrete-indiscrete-cleanup

Conversation

@danflapjax
Copy link
Collaborator

Now that a feature was added to make redundant properties easier to spot, I went through and removed all the derivable instances of non-discrete and non-indiscrete traits, as these are uninteresting.

Copy link
Collaborator

@felixpernegger felixpernegger left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

good

@prabau prabau merged commit 834a9df into main Mar 13, 2026
1 check passed
@prabau prabau deleted the discrete-indiscrete-cleanup branch March 13, 2026 23:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants