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.