Skip to content

[Merged by Bors] - feat: Init.Data.Ordering.Basic#568

Closed
pechersky wants to merge 4 commits intomasterfrom
pechersky/port-init-data-ordering
Closed

[Merged by Bors] - feat: Init.Data.Ordering.Basic#568
pechersky wants to merge 4 commits intomasterfrom
pechersky/port-init-data-ordering

Conversation

@pechersky
Copy link
Copy Markdown
Contributor

@pechersky pechersky commented Nov 11, 2022

No description provided.

@pechersky pechersky requested a review from digama0 November 11, 2022 01:19
@pechersky
Copy link
Copy Markdown
Contributor Author

@digama0 does this belong in std4?

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 11, 2022

I think the answer for a lot of stuff is going to be "yes, probably this belongs in Std", but that can all happen later, as Std grows and needs stuff.

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 11, 2022

bors merge

bors bot pushed a commit that referenced this pull request Nov 11, 2022
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Nov 11, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: Init.Data.Ordering.Basic [Merged by Bors] - feat: Init.Data.Ordering.Basic Nov 11, 2022
@bors bors bot closed this Nov 11, 2022
@bors bors bot deleted the pechersky/port-init-data-ordering branch November 11, 2022 02:34
bors bot pushed a commit that referenced this pull request Nov 18, 2022
mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

- [x] depends on: #568 
- [x] depends on: #562 



Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants