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

[Merged by Bors] - chore(algebra/order): enable dot syntax#3643

Closed
urkud wants to merge 3 commits intomasterfrom
le-lt-dot
Closed

[Merged by Bors] - chore(algebra/order): enable dot syntax#3643
urkud wants to merge 3 commits intomasterfrom
le-lt-dot

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Jul 31, 2020

Add dot syntax aliases to some lemmas about order (e.g.,
has_le.le.trans). Also remove lt_of_le_of_ne' (was equivalent
to lt_of_le_of_ne).

Part of #3640

@urkud
chore(algebra/order): enable dot syntax
9841b2b 
Add dot syntax aliases to some lemmas about order (e.g.,
`has_le.le.trans`). Also remove `lt_of_le_of_ne'` (was equivalent
to `lt_of_le_of_ne`).
@urkud urkud added the awaiting-review The author would like community review of the PR label Jul 31, 2020
@digama0
Copy link
Copy Markdown
Member

digama0 commented Aug 1, 2020 •
edited
Loading

lt_of_le_of_ne' avoids classical.choice. It was originally intended to be moved to core (or vice versa) replacing the original proof when order theory in core gets sorted out.

Side note: Please don't delete proofs unless you know the reason they were added. Besides avoiding axioms, another reason there might be an apparently redundant proof is to provide an alternate proof of a result.

@urkud
Copy link
Copy Markdown
Member Author

urkud commented Aug 1, 2020 •
edited
Loading

Sorry, I should've run git log -S before opening PR. leanprover-community/lean#428

This was referenced Aug 1, 2020
Closed
Closed
@sgouezel
Copy link
Copy Markdown
Collaborator

sgouezel commented Aug 1, 2020

Can you just add a minimalistic file-level docstring, with an illustration of the use of dot notation? This will be so helpful that I would like to have a pointer to give on Zulip when needed.

@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Aug 1, 2020
@bryangingechen bryangingechen mentioned this pull request Aug 1, 2020
Closed
@urkud urkud added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 1, 2020
urkud
urkud commented Aug 1, 2020
View reviewed changes
@sgouezel
Copy link
Copy Markdown
Collaborator

sgouezel commented Aug 2, 2020

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Aug 2, 2020
bors bot pushed a commit that referenced this pull request Aug 2, 2020
@urkud
chore(algebra/order): enable dot syntax (#3643)
e41d3ea 
Add dot syntax aliases to some lemmas about order (e.g.,
`has_le.le.trans`). Also remove `lt_of_le_of_ne'` (was equivalent
to `lt_of_le_of_ne`).
@bors
Copy link
Copy Markdown

bors bot commented Aug 2, 2020

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Aug 2, 2020
@urkud
chore(algebra/order): enable dot syntax (#3643)
f2db6a8 
Add dot syntax aliases to some lemmas about order (e.g.,
`has_le.le.trans`). Also remove `lt_of_le_of_ne'` (was equivalent
to `lt_of_le_of_ne`).
@bors
Copy link
Copy Markdown

bors bot commented Aug 2, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(algebra/order): enable dot syntax [Merged by Bors] - chore(algebra/order): enable dot syntax Aug 2, 2020
@bors bors bot closed this Aug 2, 2020
@bors bors bot deleted the le-lt-dot branch August 2, 2020 10:00
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

No reviews

Assignees

No one assigned

Labels

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.

3 participants

@urkud @digama0 @sgouezel