Zulip Chat Archive
Stream: PR reviews
Topic: removing things labeled helper
Matthew Ballard (May 09 2024 at 20:25):
#12786 removes some porting notes from Order.RelIso and unnecessary CoeFun instance.
#12789 removes a helper instance which is just Semiring.toModule
Neither materially affects performance.
Last updated: May 02 2025 at 03:31 UTC