Commit 2024-10-01 20:15 96ac52ff

View on Github →

chore(*.ModEq): reduce dependencies (#17154) Both Nat.ModEq and Int.ModEq have some spurious dependencies which can be removed by reasonable swaps of generic tactics/declarations for Nat and Int native versions (e.g. use omega more). This PR does that and makes a slouching attempt to hold back the import graph downstream of these.

Estimated changes