Skip to content

[Merged by Bors] - chore: re-port Init.Function#5859

Closed
eric-wieser wants to merge 10 commits intomasterfrom
port/Init.Function
Closed

[Merged by Bors] - chore: re-port Init.Function#5859
eric-wieser wants to merge 10 commits intomasterfrom
port/Init.Function

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

Notably this fixes the naming of comp_left and comp_right.


Open in Gitpod

@eric-wieser eric-wieser added awaiting-review mathlib-port This is a port of a theory file from mathlib. awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jul 13, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 13, 2023
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@kim-em kim-em added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 14, 2023
bors bot pushed a commit that referenced this pull request Jul 14, 2023
Notably this fixes the naming of `comp_left` and `comp_right`.



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Jul 14, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore: re-port Init.Function [Merged by Bors] - chore: re-port Init.Function Jul 14, 2023
@bors bors bot closed this Jul 14, 2023
@bors bors bot deleted the port/Init.Function branch July 14, 2023 20:45
kbuzzard pushed a commit that referenced this pull request Jul 15, 2023
Notably this fixes the naming of `comp_left` and `comp_right`.



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
bors bot pushed a commit that referenced this pull request Aug 2, 2023
This was done once in #5063, then accidentally reverted in #5859.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
kim-em added a commit that referenced this pull request Aug 3, 2023
This was done once in #5063, then accidentally reverted in #5859.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
kim-em added a commit that referenced this pull request Aug 3, 2023
This was done once in #5063, then accidentally reverted in #5859.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
kim-em pushed a commit that referenced this pull request Aug 14, 2023
Notably this fixes the naming of `comp_left` and `comp_right`.



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
kim-em added a commit that referenced this pull request Aug 14, 2023
This was done once in #5063, then accidentally reverted in #5859.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants