Markus Himmel

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

feat: Std.HashMap

1

### Preliminary PRs: - [x] #4597 - [x] #4599 - [x] #4600 - [x] #4602 - [x] #4603 - [x] #4604 - [x] #4605 - [ ] #4607 - [...

feat: additional lemmas for arrays

1

Split from #4583

feat: EquivBEq and LawfulHashable classes

3

Split from #4583 There are two open questions, opinions appreciated: - Should this material be part of `Init` or `Std`? - Should the typeclasses be in the `Std` namespace?

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

"Try this" suggestion includes trailing comments

1

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

feature request: more visible feedback when creating a new project

2

### Proposal When creating a new Lean project using mathlib from the extension, a lot of stuff happens: elan pulls in the correct Lean version, the cache tool is built...