Skip to content

Comments

chore: remove unused simp lemmas#951

Merged
zhikaip merged 2 commits intomasterfrom
unused_simp
Feb 19, 2026
Merged

chore: remove unused simp lemmas#951
zhikaip merged 2 commits intomasterfrom
unused_simp

Conversation

@zhikaip
Copy link
Collaborator

@zhikaip zhikaip commented Feb 18, 2026

I thought this will get picked up by the github build checks

@zhikaip zhikaip added the easy < 20s of review time label Feb 18, 2026
Copy link
Member

@jstoobysmith jstoobysmith left a comment

Choose a reason for hiding this comment

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

Approved. Was this emitting a warning? Likely the github workflows don't break for just warnings (rather than errors), maybe this is something we can change.

@jstoobysmith jstoobysmith added the ready-to-merge This PR is approved and will be merged shortly label Feb 19, 2026
@zhikaip
Copy link
Collaborator Author

zhikaip commented Feb 19, 2026

Approved. Was this emitting a warning? Likely the github workflows don't break for just warnings (rather than errors), maybe this is something we can change.

Yes I noticed this during build

@zhikaip zhikaip merged commit f7a48c2 into master Feb 19, 2026
3 checks passed
@zhikaip zhikaip deleted the unused_simp branch February 19, 2026 07:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

easy < 20s of review time ready-to-merge This PR is approved and will be merged shortly

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants