[Merged by Bors] - feat(data/indicator_function): add multiplicative version#6794
[Merged by Bors] - feat(data/indicator_function): add multiplicative version#6794
Conversation
This will help us add `finprod` in #6355
eric-wieser
left a comment
There was a problem hiding this comment.
I've only skimmed this, but the idea looks good to me, and I'm reasonably confident in CI's ability to catch mistakes!
kbuzzard
left a comment
There was a problem hiding this comment.
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 |
There was a problem hiding this comment.
Do we now want to normalising the spacing again? The next few lines now look a bit weird.
There was a problem hiding this comment.
I did this in the fincard branch. I'll cherry-pick this chunk tonight.
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
|
🎉 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! |
|
bors r- |
|
bors merge |
|
Pull request successfully merged into master. Build succeeded: |
We need it for
finprodfunction.mul_support#6791