Skip to content

Conversation

@nomeata
Copy link
Collaborator

@nomeata nomeata commented Dec 9, 2025

This PR removed unused imports from Try.Collect

This PR removed unused imports from Try.Collect
@nomeata
Copy link
Collaborator Author

nomeata commented Dec 9, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Dec 9, 2025

Benchmark results for e29faaa against 5326530 are in! @nomeata

No significant changes detected.

@nomeata nomeata marked this pull request as ready for review December 9, 2025 22:15
@nomeata nomeata requested a review from leodemoura as a code owner December 9, 2025 22:15
@nomeata nomeata enabled auto-merge December 9, 2025 22:15
@nomeata nomeata added this pull request to the merge queue Dec 9, 2025
Merged via the queue into master with commit 5bf5c73 Dec 9, 2025
14 of 15 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.

3 participants