feat: extensional hash maps (#8004) This PR adds extensional hash maps and hash sets under the names `Std.ExtDHashMap`, `Std.ExtHashMap` and `Std.ExtHashSet`. Extensional hash maps work like regular hash maps, except that they have extensionality lemmas which make them easier to use in proofs. This however makes it also impossible to regularly iterate over its entries.
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).