Commit 2025-04-07 01:19 411847ca

View on Github →

chore: cc uses TreeMap instead of RBMap (#23572)

Estimated changes

Modified Mathlib/Data/MLList/BestFirst.lean

Modified Mathlib/Tactic/CC/Addition.lean

Modified Mathlib/Tactic/CC/Datatypes.lean

modified def Mathlib.Tactic.CC.ACEntry.ROccs

Modified Mathlib/Tactic/CC/MkProof.lean

Modified Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean

Modified Mathlib/Tactic/Linarith/Parsing.lean