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 Data.Nat.Interval #1838

Closed
wants to merge 27 commits into from
Closed

[Merged by Bors] - feat: port Data.Nat.Interval #1838

wants to merge 27 commits into from

Conversation

joneugster
Copy link
Collaborator

@joneugster joneugster commented Jan 26, 2023 •
edited by ChrisHughes24

dupuisf and others added 23 commits January 21, 2023 20:11
@dupuisf
feat: port Order.LocallyFinite
609f786
@dupuisf
Initial file copy from mathport
46a9a4e
@dupuisf
automated fixes
8d7c11d 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@dupuisf
done up until name clash with mathlib3
318fd5e
@Ruben-VandeVelde
Merge remote-tracking branch 'origin/master' into port/Order.LocallyF…
fe46942 
…inite
@Ruben-VandeVelde
partial fixes
7495c0e
@Ruben-VandeVelde
partial fixes
3d57e3d
@Ruben-VandeVelde
fix
d25baa8
@Ruben-VandeVelde
lint
5558096
@Ruben-VandeVelde
docs
149f983
@joneugster
feat: port Data.Finset.LocallyFinite
fc155e1
@joneugster
Initial file copy from mathport
c6c9fb5
@joneugster
script output
6a3fe2a
@joneugster
update Mathlib.lean
817432b
@joneugster
Merge branch 'port/Order.LocallyFinite' into port/Data.Finset.Locally…
44d61c2 
…Finite
@joneugster
fix localised notation for Set.uIcc
7e1c712
@joneugster
fixes
7081926
@joneugster
lint
f1bfe55
@joneugster
fix
ebd5230
@joneugster
fix
77cf3a5
@joneugster
feat: port Data.Nat.Interval
c4c7a53
@joneugster
Initial file copy from mathport
1f8e306
@joneugster
script output
f8cc07f
@joneugster joneugster added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Jan 26, 2023
@semorrison semorrison added the blocked-by-other-PR This PR depends on another PR to Mathlib label Jan 26, 2023
@joneugster joneugster removed the WIP Work in progress label Jan 26, 2023
@joneugster joneugster added the awaiting-review The author would like community review of the PR label Jan 26, 2023
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Jan 26, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@ChrisHughes24
Copy link
Member

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 Jan 26, 2023
bors bot pushed a commit that referenced this pull request Jan 26, 2023
@dupuisf @Ruben-VandeVelde
@joneugster @ChrisHughes24
feat: port Data.Nat.Interval (#1838)
ad4c81e 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
@bors
Copy link

bors bot commented Jan 26, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Data.Nat.Interval [Merged by Bors] - feat: port Data.Nat.Interval Jan 26, 2023
@bors bors bot closed this Jan 26, 2023
@bors bors bot deleted the port/Data.Nat.Interval branch January 26, 2023 10:39
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
5 participants
@joneugster @semorrison @ChrisHughes24 @dupuisf @Ruben-VandeVelde