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