Skip to content

[Merged by Bors] - [Merged by Bors] - feat: port Data.Rat.Order#1116

Closed
kim-em wants to merge 67 commits intomasterfrom
data_rat_order
Closed

[Merged by Bors] - [Merged by Bors] - feat: port Data.Rat.Order#1116
kim-em wants to merge 67 commits intomasterfrom
data_rat_order

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

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

kim-em and others added 30 commits December 14, 2022 12:00
@kim-em
feat : port Data.Int.Dvd.Basic
d4bbea0
@kim-em
initial pass on Data.Rat.Defs
79c953b
@PatrickMassot
Merge branch 'master' into data_rat_defs
13a33a5
@kim-em
merge
61e8858
@kim-em
long lines
6b95eef
@kim-em
some more work
6c1bdf1
@Ruben-VandeVelde
minor fixes
d1012b8
@PatrickMassot
One more proof despite weird bug
7d0e031
@ChrisHughes24
some fixes
5e0e39f
@ChrisHughes24
Merge branch 'data_rat_defs' of https://github.com/leanprover-communi…
6ae4b7a 
…ty/mathlib4 into data_rat_defs
@PatrickMassot
Some progress
7a804fd
@arienmalec
fix for one branch of mul_def
90d7e65
@PatrickMassot
And some more
8fccdc6
@kim-em
link to #1956
6217785
@kim-em
Merge remote-tracking branch 'origin/master' into data_rat_defs
dffd237
@kim-em
some fixes
e9ae68d
@kim-em
fixes
4a8506c
@kim-em
fix
9754771
@kim-em
fix
af8b8d8
@kim-em
prove zero_mul, mul_zero
530e97e
@kim-em
don't override instances
38c1a3e
@kim-em
sub_eq_add_neg
35e4304
@kim-em
the easy branch of add_def'
d88d908
@kim-em
hrm
6ccbe51
@kim-em
cleanup
7d4540a
@kim-em
more casts... these seem suspicious
1420750
@kim-em
golf
2a57e47
@kim-em
Merge remote-tracking branch 'origin/master' into data_rat_defs
52123c7
@kim-em
fix two branches of inv_def
f127d13
@kim-em
finish inv_def
998002c
@kim-em kim-em added WIP Work in progress blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Dec 20, 2022
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 20, 2022
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Dec 20, 2022

This PR/issue depends on:

@digama0 digama0 added awaiting-review and removed WIP Work in progress labels 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.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>
@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.Order [Merged by Bors] - feat: port Data.Rat.Order Dec 20, 2022
@bors bors bot closed this Dec 20, 2022
@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 [Merged by Bors] - feat: port Data.Rat.Order [Merged by Bors] - [Merged by Bors] - feat: port Data.Rat.Order Dec 20, 2022
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>
@int-y1 int-y1 deleted the data_rat_order branch April 16, 2023 18:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

Labels

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 @jcommelin @digama0 @PatrickMassot @Ruben-VandeVelde @ChrisHughes24 @arienmalec