Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Name enhancement erasion_op => absorbing_op #7211

Open
Kannen opened this issue May 12, 2021 · 3 comments
Open

Name enhancement erasion_op => absorbing_op #7211

Kannen opened this issue May 12, 2021 · 3 comments
Labels
S-needs-discussion Status: Needs further discussion before merging or work can be started

Comments

@Kannen
Copy link

Kannen commented May 12, 2021

There is the identity_op lint that fires on operations as 1*x

The name identity correspond to the accepted term, see Wikipedia/identity element.

There is the erasing_op lint that fires on operations as 0*x
But the term erasing is vague, e.g.: could it mean type erasure??
There is a precise word for that too: 0 is an absorbing element: see Wikipedia/absorbing element

@giraffate giraffate added the S-needs-discussion Status: Needs further discussion before merging or work can be started label May 13, 2021
@HKalbasi
Copy link
Member

@giraffate any disagreement? How much harm does renaming a lint?

@giraffate
Copy link
Contributor

No, I just wanted some more opinions about this.

@HKalbasi
Copy link
Member

#2845 suggest merging those and some more lints to unused_operations. I think unnecessary_operation is a better name for that merged lint but this is already a lint which is completely different.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
S-needs-discussion Status: Needs further discussion before merging or work can be started
Projects
None yet
Development

No branches or pull requests

3 participants