Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: EquivBEq and LawfulHashable classes #4607

Merged
merged 1 commit into from
Jul 4, 2024
Merged

feat: EquivBEq and LawfulHashable classes #4607

merged 1 commit into from
Jul 4, 2024

Conversation

TwoFX
Copy link
Member

@TwoFX TwoFX commented Jul 1, 2024

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?

@TwoFX TwoFX mentioned this pull request Jul 1, 2024
Merged
10 tasks
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 1, 2024 12:16 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 1, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Jul 1, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-07-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-07-01 12:26:11)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 554e7234330cf06efffe0cb52092e783a27561cc --onto 4d0b7cf66c140dd83f8c8634293047335a385026. (2024-07-02 08:29:48)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8959b2ca87a67cb88ab0828db3672384ad7302fe --onto 4d0b7cf66c140dd83f8c8634293047335a385026. (2024-07-02 12:40:50)

@kim-em
Copy link
Collaborator

kim-em commented Jul 2, 2024

I think this should be in the root namespace, at least for now.

Let's keep this in Init.

@TwoFX TwoFX force-pushed the markus/std_classes branch from 4ecadd8 to edba8bc Compare July 2, 2024 08:14
@TwoFX
Copy link
Member Author

TwoFX commented Jul 2, 2024

Okay, I have moved the classes to Init.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 2, 2024 08:41 Inactive
@TwoFX TwoFX force-pushed the markus/std_classes branch from e763472 to b2d388d Compare July 2, 2024 12:28
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 2, 2024 12:33 Inactive
@TwoFX TwoFX added the will-merge-soon …unless someone speaks up label Jul 3, 2024
@TwoFX TwoFX added this pull request to the merge queue Jul 4, 2024
Merged via the queue into master with commit d4e141e Jul 4, 2024
15 checks passed
github-merge-queue bot pushed a commit that referenced this pull request Jul 5, 2024
@TwoFX
feat: Std.HashMap (#4583)
3e0ea76 
### Preliminary PRs:

- [x] #4597 
- [x] #4599
- [x] #4600
- [x] #4602
- [x] #4603
- [x] #4604
- [x] #4605
- [x] #4607
- [x] #4627
- [x] #4629 

### Quick overview over API/naming changes compared to `Lean.HashMap`
and `Batteries.HashMap`:
#### Lean

* `find?` -> `get?`/`getElem?`
* `find!` -> `get!`/`gtetElem!`
* `findD` -> `getD`
* `findEntry?` -> not implemented for now
* `insert'` -> `containsThenInsert` (order reversed in result)
* `insertIfNew` -> `getThenInsertIfNew?` (order reversed in result)
* `numBuckets` -> `Internal.numBuckets`
* `ofListWith` -> not implemented for now
* `Array.groupByKey` -> not implemented for now
* `merge` -> not implemented for now, but you can use `insertMany`

#### Batteries

* `modify` -> not implemented for now
* `mergeWith` -> not implemented for now
* `mergeWithM` -> not implemented for now
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

Assignees
No one assigned
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@TwoFX @leanprover-community-mathlib4-bot @kim-em