Commit 2023-11-13 12:59 5c23e7f8
View on Github →fix: remove unused arguments (#8380) These are split from #8226 (and subsequent changes in #8366), and arise from the fact the latest Lean is better at detecting these due to better abstraction. I can't comment on whether any of these should be concerning, but putting them in a small commit makes it easier for someone to find and review them later.