Skip to content

perf: improve some instances in Subgroup#7431

Closed
ChrisHughes24 wants to merge 5 commits intomasterfrom
SubgroupInstPerfCH
Closed

perf: improve some instances in Subgroup#7431
ChrisHughes24 wants to merge 5 commits intomasterfrom
SubgroupInstPerfCH

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member


Open in Gitpod

@ChrisHughes24 ChrisHughes24 added WIP Work in progress awaiting-author A reviewer has asked the author a question or requested changes. labels Sep 29, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member Author

!bench

@ChrisHughes24 ChrisHughes24 changed the title perf: improve some instance in Subgroup perf: improve some instances in Subgroup Sep 29, 2023
@leanprover-bot
Copy link
Copy Markdown
Collaborator

Here are the benchmark results for commit f3fdf20.
The entire run failed.
Found no significant differences.

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 25, 2024
@YaelDillies YaelDillies deleted the SubgroupInstPerfCH branch August 12, 2025 05:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author A reviewer has asked the author a question or requested changes. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) WIP Work in progress

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants