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

feat: more min/max lemmas for Nat #196

Merged
merged 5 commits into from
Nov 1, 2023
Merged

feat: more min/max lemmas for Nat #196

merged 5 commits into from
Nov 1, 2023

Conversation

fgdorais
Copy link
Collaborator

@fgdorais fgdorais commented Jul 23, 2023 •
edited
Loading

@fgdorais fgdorais force-pushed the nat-min-max branch 2 times, most recently from 9237a44 to 2e0f987 Compare July 28, 2023 03:49
@fgdorais fgdorais added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Aug 21, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Oct 19, 2023
digama0
digama0 reviewed Oct 19, 2023
View reviewed changes
@digama0
Copy link
Member

digama0 commented Oct 19, 2023

Deprecated Nat.zero_min, Nat.min_zero, Nat.zero_max, Nat.max_zero because min/max are not infix operators.

Naming is not based on the notation of operators. min/max are binary operators, so this is a perfectly valid way to name lemmas.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Oct 19, 2023
@fgdorais
Copy link
Collaborator Author

Updated to enforce naming conventions. Mathlib patch now in CI.

@fgdorais fgdorais mentioned this pull request Nov 1, 2023
Closed
2 tasks
@digama0 digama0 merged commit b541ac2 into leanprover-community:main Nov 1, 2023
@fgdorais fgdorais deleted the nat-min-max branch November 5, 2023 04:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 digama0 left review comments

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@fgdorais @digama0 @leanprover-community-mathlib4-bot