Commit 2025-04-25 13:55 5fd096bd
View on Github →chore: use TreeMap in to_additive (#24366)
This PR avoids use of Lean.RBMap
in the implementation of to_additive
, where the new Std.TreeMap
suffices.
chore: use TreeMap in to_additive (#24366)
This PR avoids use of Lean.RBMap
in the implementation of to_additive
, where the new Std.TreeMap
suffices.