Skip to content

Remove redundant casts - #187

Merged
zesterer merged 1 commit into
zesterer:masterfrom
FranciscoTGouveia:remove-casts
Aug 7, 2026
Merged

zesterer merged 1 commit into
zesterer:masterfrom
FranciscoTGouveia:remove-casts

Conversation

@FranciscoTGouveia

Copy link
Copy Markdown
Contributor

If I am not overlooking anything, I believe these casts are redundant and can thus be safely removed.

For reference, this change was found by an optimizer developed as a research project.

CC @nunoplopes

@zesterer

zesterer commented Aug 7, 2026

Copy link
Copy Markdown
Owner

Thanks!

@zesterer
zesterer merged commit 8c18b2b into zesterer:master Aug 7, 2026
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants