You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Working on #1711 / #2182 (and specifically: the knock-on changes arising from streamlining Data.Nat.DivMod) drew my attention to the very (overly!?) involved instance-based reasoning in Data.Rational.Properties concerning gcd and its role in the normalise function.
Suggest a careful weeding out of the accumulated cruft and verbosity there: the many examples of first proving a lemma to the effect that some quantity is n satisfies n ≢ 0, and then appealing to another lemma to turn that into an instance of NonZero n...
... a temporary, and tip-of-the-iceberg, case of which is in commit 6d819ae