Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(data/finset/basic): mem_map_equiv #6399

Closed
wants to merge 2 commits into from

Conversation

gebner
Copy link
Member

@gebner gebner commented Feb 24, 2021

This adds a version of mem_map specialized to equivs, which has a better simp-nf.


@gebner gebner added the awaiting-review The author would like community review of the PR label Feb 24, 2021
@robertylewis robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Feb 24, 2021
@gebner gebner added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Feb 24, 2021
Copy link
Collaborator

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Feb 25, 2021
bors bot pushed a commit that referenced this pull request Feb 25, 2021
This adds a version of `mem_map` specialized to equivs, which has a better simp-nf.
@bors
Copy link

bors bot commented Feb 25, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/finset/basic): mem_map_equiv [Merged by Bors] - feat(data/finset/basic): mem_map_equiv Feb 25, 2021
@bors bors bot closed this Feb 25, 2021
@bors bors bot deleted the finset_congr branch February 25, 2021 07:08
b-mehta pushed a commit that referenced this pull request Apr 2, 2021
This adds a version of `mem_map` specialized to equivs, which has a better simp-nf.
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants