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

[Merged by Bors] - feat(data/indicator_function): add multiplicative version#6794

Closed
urkud wants to merge 14 commits intomasterfrom
mul-indicator
Closed

[Merged by Bors] - feat(data/indicator_function): add multiplicative version#6794
urkud wants to merge 14 commits intomasterfrom
mul-indicator

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Mar 21, 2021

@github-actions github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Mar 21, 2021
@urkud urkud added the awaiting-review The author would like community review of the PR label Mar 21, 2021
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

I've only skimmed this, but the idea looks good to me, and I'm reasonably confident in CI's ability to catch mistakes!

Copy link
Copy Markdown
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

Thank you so much for this rather large refactor.

| is_comm ("le" :: "one" :: s) := add_comm_prefix is_comm "nonpos" :: tr ff s
| is_comm ("lt" :: "one" :: s) := add_comm_prefix is_comm "neg" :: tr ff s
| is_comm ("mul" :: "support" :: s) := add_comm_prefix is_comm "support" :: tr ff s
| is_comm ("mul" :: "indicator" :: s) := add_comm_prefix is_comm "indicator" :: tr ff s
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Do we now want to normalising the spacing again? The next few lines now look a bit weird.

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

I did this in the fincard branch. I'll cherry-pick this chunk tonight.

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Mar 22, 2021
@github-actions
Copy link
Copy Markdown

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 23, 2021
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

@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+`.) merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed awaiting-review The author would like community review of the PR labels Mar 23, 2021
@urkud
Copy link
Copy Markdown
Member Author

urkud commented Mar 24, 2021

bors r-
merge conflicts

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 24, 2021
@bryangingechen bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes delegated The PR author may merge after reviewing final suggestions. and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Mar 24, 2021
@urkud urkud removed the awaiting-author A reviewer has asked the author a question or requested changes label Mar 25, 2021
@urkud
Copy link
Copy Markdown
Member Author

urkud commented Mar 25, 2021

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Mar 25, 2021
bors bot pushed a commit that referenced this pull request Mar 25, 2021
@bors
Copy link
Copy Markdown

bors bot commented Mar 25, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/indicator_function): add multiplicative version [Merged by Bors] - feat(data/indicator_function): add multiplicative version Mar 25, 2021
@bors bors bot closed this Mar 25, 2021
@bors bors bot deleted the mul-indicator branch March 25, 2021 07:15
b-mehta pushed a commit that referenced this pull request Apr 2, 2021
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

delegated The PR author may merge after reviewing final suggestions. 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

Development

Successfully merging this pull request may close these issues.

5 participants