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

[Merged by Bors] - refactor(data/fin/basic): fin refactor to use ne_zero #18107

Closed
wants to merge 30 commits into from
Closed

[Merged by Bors] - refactor(data/fin/basic): fin refactor to use ne_zero #18107

wants to merge 30 commits into from

Conversation

ChrisHughes24
Copy link
Member

@ChrisHughes24 ChrisHughes24 commented Jan 9, 2023 •
edited
Loading

Refactor as suggested on Zulip

I also generalized as many lemmas as I could to use ne_zero n instead of fin (n + 1)

Open in Gitpod

@ChrisHughes24 ChrisHughes24 added the awaiting-CI The author would like to see what CI has to say before doing more work. label Jan 9, 2023
eric-wieser
eric-wieser reviewed Jan 9, 2023
View reviewed changes
src/data/fin/basic.lean Outdated Show resolved Hide resolved
eric-wieser
eric-wieser reviewed Jan 9, 2023
View reviewed changes
src/data/fin/basic.lean Outdated Show resolved Hide resolved
@ChrisHughes24 ChrisHughes24 changed the title feat(data/fin/basic): fin refactor to use ne_zero refactor(data/fin/basic): fin refactor to use ne_zero Jan 9, 2023
@ChrisHughes24 ChrisHughes24 requested a review from a team as a code owner January 9, 2023 11:56
@ChrisHughes24 ChrisHughes24 added awaiting-review The author would like community review of the PR and removed awaiting-CI The author would like to see what CI has to say before doing more work. labels Jan 9, 2023
@ChrisHughes24
Copy link
Member Author

This now builds locally

eric-wieser
eric-wieser reviewed Jan 9, 2023
View reviewed changes
src/data/zmod/defs.lean Outdated Show resolved Hide resolved
@ChrisHughes24 ChrisHughes24 requested a review from a team as a code owner January 9, 2023 15:47
FR-vdash-bot
FR-vdash-bot reviewed Jan 10, 2023
View reviewed changes
Copy link
Collaborator

@FR-vdash-bot FR-vdash-bot left a comment

Choose a reason for hiding this comment

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

Updating docstrings.

src/data/fin/basic.lean Outdated Show resolved Hide resolved
src/data/fin/basic.lean Outdated Show resolved Hide resolved
src/data/fin/basic.lean Outdated Show resolved Hide resolved
src/data/fin/basic.lean Outdated Show resolved Hide resolved
src/data/fin/basic.lean Outdated Show resolved Hide resolved
@ChrisHughes24 @FR-vdash-bot
Apply suggestions from code review
04e990b 
Co-authored-by: negiizhao <egresf@gmail.com>
ChrisHughes24 and others added 4 commits January 10, 2023 11:19
@ChrisHughes24 @FR-vdash-bot
Apply suggestions from code review
ce93310 
Co-authored-by: negiizhao <egresf@gmail.com>
@ChrisHughes24 @FR-vdash-bot
Update src/data/fin/basic.lean
ac387b0 
Co-authored-by: negiizhao <egresf@gmail.com>
@ChrisHughes24
fix test
e290557
@ChrisHughes24
fix test
468622e
@ChrisHughes24
Copy link
Member Author

bors r+

@bors
Copy link

bors bot commented Jan 10, 2023

👎 Rejected by label

@ChrisHughes24 ChrisHughes24 removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jan 10, 2023
@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jan 10, 2023
@ChrisHughes24
Copy link
Member Author

bors r+

@bors
Copy link

bors bot commented Jan 10, 2023

Canceled.

@ChrisHughes24 ChrisHughes24 added awaiting-CI The author would like to see what CI has to say before doing more work. and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Jan 10, 2023
@jcommelin jcommelin mentioned this pull request Jan 11, 2023
Closed
2 tasks
@riccardobrasca
Copy link
Member

The simp_nf linter was complaining

#check @fin.coe_of_nat_eq_mod /- simp can prove this:
  by simp only [fin.coe_of_nat_eq_mod']
One of the lemmas above could be a duplicate.

I switched the order of fin.coe_of_nat_eq_mod and fin.coe_of_nat_eq_mod'.

@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jan 11, 2023
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jan 11, 2023
bors bot pushed a commit that referenced this pull request Jan 11, 2023
@ChrisHughes24 @riccardobrasca
refactor(data/fin/basic): fin refactor to use ne_zero (#18107)
0bd2ea3 
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
@bors
Copy link

bors bot commented Jan 11, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(data/fin/basic): fin refactor to use ne_zero [Merged by Bors] - refactor(data/fin/basic): fin refactor to use ne_zero Jan 11, 2023
@bors bors bot closed this Jan 11, 2023
@bors bors bot deleted the fin_refactor branch January 11, 2023 18:25
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@FR-vdash-bot FR-vdash-bot FR-vdash-bot left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. 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
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@ChrisHughes24 @riccardobrasca @jcommelin @eric-wieser @FR-vdash-bot @leanprover-community-bot-assistant