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

[Merged by Bors] - feat: port Logic.Equiv.Array #1733

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat: port Logic.Equiv.Array #1733

wants to merge 12 commits into from

Conversation

maxwell-thum
Copy link
Collaborator

@maxwell-thum maxwell-thum commented Jan 20, 2023 •
edited by Parcly-Taxel

Open in Gitpod

@maxwell-thum
feat: port Logic.Equiv.Array
15ac109
@maxwell-thum
Initial file copy from mathport
ec5a7ff
@maxwell-thum
automated fixes
6fbdf07 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@maxwell-thum maxwell-thum added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. help-wanted The author needs attention to resolve issues labels Jan 20, 2023
@maxwell-thum
Copy link
Collaborator Author

I think this may be a bit out of my range. I'm not at all familiar with the differences between Arrays in Lean 3 and 4.

@maxwell-thum
Copy link
Collaborator Author

Oh, but if you do understand that stuff, this file is very short.

@prakol16 prakol16 mentioned this pull request Feb 18, 2023
Closed
@Parcly-Taxel Parcly-Taxel added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Mar 15, 2023
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Apr 9, 2023
@Ruben-VandeVelde
Copy link
Collaborator

We're not porting this; see #2194.

@thorimur
Copy link
Collaborator

Reopening this PR and rewriting in terms of Array as per zulip!

@thorimur thorimur reopened this Jun 26, 2023
@thorimur
delete: remove equivs and add porting note
988c9f3
@thorimur
introduce arrayEquivList; port dependents
b7b0909 
* this enables `Array.encodable` and `Array.countable`
@thorimur
docs: update porting note
93cde0b
@thorimur
remove: instances for Traversable (Array α)
165a0a9 
* and `IsLawfulTraversable (Array α)`
* added porting note explaining rationale
@thorimur
docs: update module string
8f008af
@thorimur
docs: fix typo (Traverse -> Traversable)
603294b
@thorimur
clean up arrayEquivList
ccf6bce
@thorimur
docs: tweaks
002da95 
* Traversable porting note wording
* restore lost commented-out line of code
* remove extra newline
@thorimur thorimur added awaiting-review The author would like community review of the PR and removed help-wanted The author needs attention to resolve issues WIP Work in progress please-adopt labels Jun 27, 2023
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jun 27, 2023
bors bot pushed a commit that referenced this pull request Jun 27, 2023
@maxwell-thum @Parcly-Taxel @thorimur
feat: port Logic.Equiv.Array (#1733)
c660824 
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
@bors
Copy link

bors bot commented Jun 27, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: port Logic.Equiv.Array [Merged by Bors] - feat: port Logic.Equiv.Array Jun 27, 2023
@bors bors bot closed this Jun 27, 2023
@bors bors bot deleted the port/Logic.Equiv.Array branch June 27, 2023 15:51
semorrison pushed a commit that referenced this pull request Jun 28, 2023
@maxwell-thum @Parcly-Taxel
@thorimur @semorrison
feat: port Logic.Equiv.Array (#1733)
26acc7e 
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
kbuzzard pushed a commit that referenced this pull request Jul 6, 2023
@maxwell-thum @Parcly-Taxel
@thorimur @kbuzzard
feat: port Logic.Equiv.Array (#1733)
4ab3b1e 
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
semorrison pushed a commit that referenced this pull request Aug 14, 2023
@maxwell-thum @Parcly-Taxel
@thorimur @semorrison
feat: port Logic.Equiv.Array (#1733)
75cb871 
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@maxwell-thum @Ruben-VandeVelde @thorimur @jcommelin @semorrison @Parcly-Taxel