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: Dec 20 2025 at 21:32 UTC