Skip to content

[Merged by Bors] - feat: port Data.Rat.Defs and Data.Rat.Basic#998

Closed
kim-em wants to merge 54 commits intomasterfrom
data_rat_defs
Closed

[Merged by Bors] - feat: port Data.Rat.Defs and Data.Rat.Basic#998
kim-em wants to merge 54 commits intomasterfrom
data_rat_defs

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Dec 14, 2022 •
edited by github-actions bot
Loading

@kim-em kim-em added help-wanted The author needs attention to resolve issues WIP Work in progress mathlib-port This is a port of a theory file from mathlib. blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Dec 14, 2022
@PatrickMassot PatrickMassot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 14, 2022
@kim-em kim-em added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Dec 14, 2022
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 14, 2022
@hrmacbeth hrmacbeth mentioned this pull request Dec 19, 2022
Closed
11 tasks
@kim-em kim-em added awaiting-review and removed help-wanted The author needs attention to resolve issues WIP Work in progress labels Dec 19, 2022
Ruben-VandeVelde
Ruben-VandeVelde reviewed Dec 19, 2022
View reviewed changes
kim-em and others added 6 commits December 20, 2022 10:13
@kim-em
.
e14a5f5
@kim-em
lint
ce27c9c
@kim-em
cleanup
f686b22
@kim-em
cleanup
9c88004
@kim-em @Ruben-VandeVelde
Update Mathlib/Data/Rat/Basic.lean
0e2184b 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@kim-em
lint
44e0d55
@kim-em kim-em mentioned this pull request Dec 20, 2022
Closed
1 task
@kim-em kim-em changed the title feat: port Data.Rat.Defs feat: port Data.Rat.Defs and Data.Rat.Basic Dec 20, 2022
jcommelin
jcommelin approved these changes Dec 20, 2022
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin 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 merge

@kim-em kim-em added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 20, 2022
bors bot pushed a commit that referenced this pull request Dec 20, 2022
@kim-em @PatrickMassot
@Ruben-VandeVelde @ChrisHughes24 @arienmalec
feat: port Data.Rat.Defs and Data.Rat.Basic (#998)
6bc2e2c 
fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

- [x] depends on: #996 
- [x] depends on:  #1096

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Arien Malec <arien.malec@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Dec 20, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Data.Rat.Defs and Data.Rat.Basic [Merged by Bors] - feat: port Data.Rat.Defs and Data.Rat.Basic Dec 20, 2022
@bors bors bot closed this Dec 20, 2022
@bors bors bot deleted the data_rat_defs branch December 20, 2022 07:02
bors bot pushed a commit that referenced this pull request Dec 20, 2022
@kim-em @PatrickMassot
@Ruben-VandeVelde @ChrisHughes24 @arienmalec
feat: port Data.Rat.Order (#1116)
4ca7b4e 

- [x] depends on: #998 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Arien Malec <arien.malec@gmail.com>
joelriou pushed a commit that referenced this pull request Dec 20, 2022
@kim-em @PatrickMassot
@Ruben-VandeVelde @ChrisHughes24 @arienmalec @joelriou
feat: port Data.Rat.Order (#1116)
d26fdcb 

- [x] depends on: #998 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Arien Malec <arien.malec@gmail.com>
@github-actions github-actions bot mentioned this pull request Dec 21, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

@jcommelin jcommelin jcommelin approved these changes

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.

7 participants

@kim-em @Ruben-VandeVelde @jcommelin @PatrickMassot @ChrisHughes24 @arienmalec @digama0