chore: rename HashMap.remove to HashMap.erase (#4725) The name `remove` was chosen because it is more popular in mainstream programming languages, but being consistent with other Lean container types (including `Lean.HashMap` and `Batteries.HashMap`) is more important, so let's change the name while we still can.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean (documentation source: doc/make/index.md).