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

[Merged by Bors] - feat: port Data.Countable.Defs #736

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat: port Data.Countable.Defs #736

wants to merge 6 commits into from

Conversation

joelriou
Copy link
Collaborator

Mathlib SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

@joelriou joelriou added awaiting-review The author would like community review of the PR mathlib-port This is a port of a theory file from mathlib. labels Nov 26, 2022
@semorrison semorrison 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 Nov 26, 2022
joelriou and others added 3 commits November 26, 2022 20:38
@joelriou @semorrison
Update Mathlib/Data/Countable/Defs.lean
2994f7e 
Co-authored-by: Scott Morrison <scott@tqft.net>
@joelriou @semorrison
Update Mathlib/Data/Countable/Defs.lean
1c5393c 
Co-authored-by: Scott Morrison <scott@tqft.net>
@joelriou
added porting note about nolint instance_priority
e979f21
@joelriou joelriou 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 Nov 26, 2022
semorrison
semorrison reviewed Nov 27, 2022
View reviewed changes
Mathlib/Data/Countable/Defs.lean Outdated
Comment on lines 95 to 97
-- Porting note: removed @[nolint instance_priority] as
-- there is not (yet?) a linter to complain about the fact
-- that this instance always applies
Copy link
Contributor

Choose a reason for hiding this comment

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

I made leanprover-community/mathlib#17732 to see if there's anything wrong with just satisfying the linter here. Probably it is fine, but I also this doesn't really need to wait.

bors d+

@bors
Copy link

bors bot commented Nov 27, 2022

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@Ruben-VandeVelde Ruben-VandeVelde added delegated and removed awaiting-review The author would like community review of the PR labels Nov 27, 2022
@joelriou
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Nov 27, 2022
@joelriou @semorrison
feat: port Data.Countable.Defs (#736)
7c09b05 
Mathlib SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
@bors
Copy link

bors bot commented Nov 27, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Data.Countable.Defs [Merged by Bors] - feat: port Data.Countable.Defs Nov 27, 2022
@bors bors bot closed this Nov 27, 2022
@bors bors bot deleted the data_countable_defs branch November 27, 2022 09:01
rosborn added a commit that referenced this pull request Nov 27, 2022
@rosborn
Merge branch 'master' into Algebra.Order.Sub.Defs
6984444 
* master:
  feat: port Data.Countable.Defs (#736)
  chore: bump to nightly-2022-11-26 (#747)
  feat(Algebra/Ring/Units): port file (#746)
  style(Algebra/Order/Monoid/Lemmas): Update to current naming convention (#743)
  feat: stubs in ad-hoc ported files for linarith algebra requirements (#733)
  feat: port algebra.group.semiconj (#717)
  chore: make argument to mul_inv_cancel implicit (#737)
  feat(Algebra/Ring/InjSurj): port file (#734)
  chore: bump to nightly-2022-11-25 (#731)
  feat: port order.minmax (#728)
  chore: make the 'p' argument to Nat.find implicit (#730)
  feat: port Control.Basic (#588)
  feat: port data.finite.defs (#698)
  feat: port:  Data.DList.Basic (#616)
  chore: reduce imports in Algebra.Group.Defs (#727)
  chore(Algebra/Order/Hom/Basic): remove outParam (#692)
@github-actions github-actions bot mentioned this pull request Nov 29, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib that referenced this pull request Dec 1, 2022
@leanprover-community-bot
chore(*): add mathlib4 synchronization comments (#17754)
8d89a80 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.field.defs`: leanprover-community/mathlib4#668
* `algebra.group.commute`: leanprover-community/mathlib4#750
* `algebra.group_with_zero.commute`: leanprover-community/mathlib4#762
* `algebra.group_with_zero.semiconj`: leanprover-community/mathlib4#757
* `algebra.group_with_zero.units.basic`: leanprover-community/mathlib4#735
* `algebra.hom.embedding`: leanprover-community/mathlib4#764
* `algebra.order.monoid.cancel.defs`: leanprover-community/mathlib4#774
* `algebra.order.monoid.canonical.defs`: leanprover-community/mathlib4#778
* `algebra.order.monoid.defs`: leanprover-community/mathlib4#771
* `algebra.order.monoid.min_max`: leanprover-community/mathlib4#763
* `algebra.order.monoid.order_dual`: leanprover-community/mathlib4#786
* `algebra.order.sub.defs`: leanprover-community/mathlib4#732
* `algebra.regular.basic`: leanprover-community/mathlib4#758
* `algebra.ring.commute`: leanprover-community/mathlib4#759
* `algebra.ring.regular`: leanprover-community/mathlib4#795
* `algebra.ring.semiconj`: leanprover-community/mathlib4#751
* `control.applicative`: leanprover-community/mathlib4#798
* `control.functor`: leanprover-community/mathlib4#612
* `control.monad.basic`: leanprover-community/mathlib4#752
* `data.countable.defs`: leanprover-community/mathlib4#736
* `data.int.units`: leanprover-community/mathlib4#807
* `data.nat.basic`: leanprover-community/mathlib4#729
* `data.nat.psub`: leanprover-community/mathlib4#806
* `data.nat.units`: leanprover-community/mathlib4#805
* `data.pi.algebra`: leanprover-community/mathlib4#564
* `data.prod.lex`: leanprover-community/mathlib4#783
* `logic.embedding.basic`: leanprover-community/mathlib4#700
* `logic.equiv.option`: leanprover-community/mathlib4#674
* `order.bounded_order`: leanprover-community/mathlib4#697
* `order.with_bot`: leanprover-community/mathlib4#776
* `order.disjoint`: leanprover-community/mathlib4#773
* `order.min_max`: leanprover-community/mathlib4#728
* `order.prop_instances`: leanprover-community/mathlib4#792
* `order.rel_iso.basic`: leanprover-community/mathlib4#772
@github-actions github-actions bot mentioned this pull request Dec 2, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

Assignees
No one assigned
Labels
delegated mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@joelriou @semorrison @Ruben-VandeVelde